perm filename PROP[P,JRA] blob
sn#443530 filedate 1979-05-22 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00025 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00003 00002 .begin "quotes" indent 8,8,8 single spaceturn on "→"
C00023 00003 .sec(History)
C00046 00004 .sec(Specification Language)
C00072 00005 .sec(Logic Programming versus Synthesis,,,P16:)
C00084 00006 .sec(Intermediate Language)
C00101 00007 .sec(Mapping From Input Specification to Intermediate Form)
C00118 00008 .sec(Correctness of the Mapping to Intermediate Form)
C00137 00009 .sec(Mapping the Intermediate Language to LISP)
C00142 00010 .sec(Correctness of the Mapping to LISP Program)
C00170 00011 .sec(Adding a New Target Language,,,P17:)
C00194 00012 .sec(Implementation Notes)
C00204 00013 .sec(Conclusions and Further Research)
C00219 00014 .bib
C00235 00015 .sec(Appendix A: Sample Specifications)
C00273 00016 .sec(Appendix B: Specification of a Program Synthesis System,,,P15:)
C00300 00017 .sec(Appendix C: Listing of the System)
C00310 00018 .next page
C00324 00019 .next page
C00358 00020 .next page
C00361 00021 .next page
C00373 00022 .next page
C00384 00023 .next page
C00438 00024 .ss(Listing of Pascal Implementation,,P14:)
C00465 00025 .next page
C00490 ENDMK
C⊗;
.begin "quotes" indent 8,8,8; single space;turn on "→"
.sec(Introduction)
.TURN ON "#";
"Software is 5%3∩%1 of the USAF's budget, 6%3∩%1 of NASA's budget and is a 10 billion
dollar a year industry (over 1%3∩%1 of the GNP)."
.nofill
→Standish [S 74]##########
.fill
.group skip 2
"Of the estimated DOD software cost of $2.5 billion previously identified,
38%3∩%1 was for analysis, 15%3∩%1 for coding, and 47%3∩%1 for validation according to the
Air Force study. ARPA is spending annually $3.5 million developing techniques to
enable the computer itself to write and debug programs, given only a specificaion
of the problem and the results desired."
.nofill
→Lukasik [L 73]##########
.fill
.group skip 2
"The one invariant in the computer field - whether mainframe, mini, or micro -
is increasing software costs. ...75 percent of the mainframe system dollar
currently goes for software. ...Systems software typically represents 50 percent
of the mini manufacturer's development budget (hardware costing 40 percent and
services making up the remaining 10 percent). ...software costs tend to dominate
in under-100-unit quantities - even on micros."
.nofill
→Davis [D 78b]##########
.fill
.end "quotes"
.group skip 2
.fp
Software is expensive and too often bug ridden. "Debugging" is still the most
commonly used method of increasing confidence in the correctness of a program.
As indicated by the statistics above, validation of the correctness of programs is
a difficult and expensive task.
Many approaches have been proposed
to ensure reliable programs, some dealing with the programming task and others
with proving a completed program does what is intended. Verification techniques
have been developed to prove that a program meets its specifications.
Several attempts have been made to provide automatic verification systems. Some
of these systems are good at proving verification conditions for a specific
problem domain, employing strategies that are geared to that domain; however, the
ability to handle problems in a new subject domain typically requires extensive
modifications of the system.
A much harder problem is discovery of the verification conditions to be proved.
One must find assertions (statements of first order logic) that characterize
the desired behavior of the program.
It is difficult enough to read someone else's program and
determine what is actually going on, let alone
figure out what the programmer had intended to do.
Even when verification
is done by the original programmer, we are asking a lot. This person must
be able (assuming a structured approach to the task) to move from logical
assumptions about the problem domain (whether or not these are
stated formally) to an implementation in a programming language, and then back
again to the logical base as a source of assertions from which the verification
conditions can be derived.
It is possible to generate some of these assertions automatically from the
text of the program. Usually the programmer supplies the critical assertions
on which his program was based, letting the machine fill in the necessary
details. However, one might question the validity of this approach.
A "proof of correctness" is really just a proof of equivalence of two
specifications of the problem, one expressed in logic, the other in a programming
language. If we derive the assertions (manually or automatically) from the
program itself, then we lose the redundancy of the two specifications; i.e., we
lose the basis of our confidence that the verification provides an
indication of true correctness.
Furthermore, if verification fails, several explanations are possible. Perhaps
the program is incorrect; perhaps the specifications are incorrect or
incomplete; perhaps the verifier is incorrect or not sufficiently powerful to
find a proof even though one does exist. If verification is successful, then
again several explanations are possible. Perhaps we have a correct program;
perhaps the verifier has made a mistake.
Assuming that the verifier contains no bugs, we have a proof that the program
meets its specifications, but the specifications may not be an accurate
embodiment of what we had in mind.
Therefore several researchers, the author included, feel that a specification of
the task should be written %2before%1 a program is written to acomplish the task.
The specification should be written in a high level language
that enables one to describe what is to be accomplished, indicating functional
relationships without having to consider computational details. Such a specification,
in which only the abstract description of the problem is required, is less prone
to error than a typical programming language specification in which every detail of
the computation must be provided. The problems of incomplete or incorrect
specifications do not go away, however we claim they are more tractable with this
approach.
Program synthesis is the generation of a computational specification of a problem or
task from a descriptive specification. Again, we do not have the redundancy
of two specifications, one descriptive and one computational, both written
by the programmer, but we feel, as discussed above, that the descriptive
specification is less prone to error. Several approaches to program synthesis
are currently being investigated. We shall review them briefly here; more
detail is given in the section on historical background.
The field of programming methodology has offered a great deal of assistance,
pointing out ways to write a program. Most notable and generally accepted
is Dijkstra's approach of "structured programming", also called "stepwise
refinement" (Wirth), of the
problem. Although intended as a discipline for humans to follow, it also
provides guidelines that can be elaborated to direct programming by the
computer itself, perhaps with human intervention.
Several investigators have taken a deductive approach to the stepwise refinement
process. The computer is given specific rules by which it can rewrite statements
syntactically while maintaining equivalent meaning.
This kind of program synthesis is closely related to program transformation.
The intent of
a program transformation system is to make the given program more efficient
while preserving its meaning. A typical transformation is one that
replaces recursion by iteration, although this does not always
result in greater efficiency. In a synthesis system, a descriptive statement
in a specification language is transformed into an operational statement in a
programming language. The specification language may be a superset of the
target programming language. The system successively refines a high level
description into a lower level (computational) description.
Less formal techniques have also found favor. Natural language dialogues have
been used to describe a problem to the computer. The user of this kind of
system specifies the task at a general level, filling in the details as requested
by the computer.
Still other approaches employ specification by example. Some systems synthesize
.group
.pt24
programs from sample input-output pairs. For example, the pair
.pt24
.begin center
(a (b c) d) => (d (b c) a)
.end
.apart
.pt24
.fp
might indicate a procedure to reverse the elements in
a list. It might also represent a procedure to switch the first and last
elements of a list; thus, one must be sure to provide a sufficient set of
examples to determine the desired function.
Another attempt at synthesis by example provides sample execution traces.
For example, the sequence
.pt24
.begin center
(4 14) => (2 4) => (0 2) => 2
.end
.pt24
.fp
might suggest the Euclidean algorithm for finding the greatest common divisor of
two integers.
Each of the techniques mentioned above have been investigated as a means to
synthesize programs in a specific target language.
It is our thesis that the synthesis of an algorithm is a
target-language-independent
process. We have implemented a system to generate programs from logic specifications.
The system is "reasonably" target-language-independent, as will be explained
later on. The specifications are first translated into an intermediate language
and then a program is generated from the intermediate form. We drop the word
"synthesis" and use program "generation" instead to avoid any misunderstanding
of the claims being made.
The specification
language for this system includes a subset of first-order Predicate
Calculus known as Horn Clauses.
The specifications we require are "descriptive" in that
they specify the logic of the program without specifying the control, but they are
also, in part, "computational" in that the Horn clauses could be "run" as programs
given a complete theorem prover, or logic interpreter.
The system was implemented in MACLISP on a DEC KL10 at the Stanford Artificial
Intelligence Laboratory. In this dissertation we describe the implementation
and prove that it provides a valid way to derive correct programs. This is
accomplished by proving that the top level mappings from specification to
intermediate language to target program (the proof is for the mapping to LISP)
are correct; the entire implementation is not proved correct.
We begin by giving a brief history of the approaches taken by other investigators
in this area, and then describe the system invented by the author.
We formally describe the specification language via a
context-free description of the syntax (see {yon (P3)})
and an axiomatic specification of the semantics (see {yon (P2)}).
Motivation for requiring particular items in the
specification is provided as well.
The relationship between a specification and a program written for a logic
interpreter is explored in {yonsec (P16)},{yon (P1)}).
We then describe the intermediate language in detail, again supplying a context-free
grammar for the syntax (see {yon (P4)}),
and the axiomatic semantics (see {yon (P5)}).
The mapping from specification language to intermediate language is described
by means of a function %dI%1, for %3internalize%1, and we prove that this mapping
preserves the axiomatic semantics of the specifications.
We then describe
the mapping from the intermediate language
to LISP and prove that the semantics is again preserved by the translation.
In {yonsec (P17)}, we describe how to extend the system to handle generation of
programs in more languages. The additions required for each new language are
referred to as a "back end" for that language.
The implementation of the "back end" for LISP and that for Pascal are also discussed.
We include some notes on the implementation and then discuss the conclusions that
can be drawn from this effort, as well as topics of further research that were
suggested by the project.
The appendices include several sample specifications and the programs generated
from them, the specification of a program generation system, and the listing
of the entire system along with the code that implements the "back end" for
LISP and that for Pascal.
This system described is unique in its ability to generate programs in more than
one language. The recipe provided explains how to construct the additions
required for any new language. Given the back-end describing a particular
target language, we can synthesize the system itself in the language,
making it immediately portable. More importantly, it provides a means of
obtaining correct programs that is decidedly less painful than verification.
The user is still required to specify the logic of a program, but the language
used in the specification frees the user from concerns of representation and
implementation.
The sobering fact remains that regardless of how (or when)
we arrive at specifications for a program, we can have no guarantee of their
correctness (in the sense that we have both a true and complete specification
of the problem we had in mind), and any attempt at verification of a program
is simply a
proof of equivalence of program and specifications. We simply do the best
we can to increase our confidence that our programs accomplish
their intended purpose.
.sec(History)
Computer scientists have always looked for ways to make the programming task
easier and less prone to error. The natural way to accomplish this is by using
the computer itself as much as possible to do its own coding.
The theoretical foundation for automatic programming was established by
Kleene [K 52]
in the 1940's. Kleene proved that if the existence of a number satisfying
certain properties can be proven in a formal intuitionist system,
⊗↓An intuitionist system allows only constructive proofs. See [K 52].← then the
definition of a function computing that number can be extracted from the proof.
The first major attempt at
automatic programming was the development of FORTRAN.
.group skip 2
.begin "quot" indent 8,8,8;single space;turn on "→#"
"If it were possible for the 704 to code problems for itself and produce as
good programs as human coders (but without the errors), it was clear that large
benefits could be achieved. ...The goal of the FORTRAN project was to enable the
programmer to specify a numerical procedure using a concise language like
that of mathematics and obtain automatically from this specification an
efficient 704 program to carry out the procedure."
.nofill
→Backus, et. al. [B 57]#########
.fill
.end "quot"
.group skip 2
In the 1960's
several high level languages were introduced as means of specifying problems
to the computer in a way more natural to us, letting the machine do the
coding. Over the years, our concept of "automatic programming" has changed.
We no longer consider a compiler an automatic program synthesizer.
J. R. Slagle [S 65] applied his question answering
program "DEDUCOM" to the task of generating programs. The relation between
input and output was expressed in predicate calculus. His technique was to
prove a theorem and write a program by keeping track of the substitutions
made for certain crucial variables in the course of the proof.
A similar approach was described by Waldinger [W 69]. He extended the technique
allowing branches and loops to be written. Again, specifications for the
program were described in Predicate Calculus as a relation between input and
output variables. Mechanical theorem proving techniques were used to
generate a constructive proof of the existence of output values satisfying
the specifications. A program was then extracted from the proof.
Since 1970, several approaches to program synthesis have been investigated.
The resolution theorem proving approach proved to be impractical, requiring
too much space while considering all possibilities. Lee and Chang [LC 74]
proposed to overcome the memory saturation problem with an interactive system
based on the concept of structured programming. Using the technique of
stepwise refinement, a program was generated in terms of subprograms until
each subprogram became an "atomic program", i.e. executable. At each step,
some appropriate information would be selected by the user for the computer
to use to generate a subprogram. In this way, the computer only had to
handle a small amount of information.
Many researchers abandoned resolution methods entirely in favor of deductive
systems with many rules of inference. Buchanan developed a system [B 74]
based on the program verification formalism of Hoare [ILL 75].
Input to the system was given in "frames" composed of assertions, state
descriptions, axioms and rules. A rule could be: a primitive procedure
with preconditions and postconditions specified; a definition, stating
the equivalence of two assertions; or an iterative rule specifying
conditions that, if satisfied, would justify the assembly of a "while"
loop to achieve the associated goal. The input specifications were rather
complicated. An iterative rule involved specifying a name, a basis assertion,
a loop invariant, an iteration step assertion, an iterative goal, a loop
control test, and an output assertion (the last two could possibly be the
same as the iterative goal). It was also possible to give advice to the system
interactively, to guide the synthesis process. This system could automatically
generate conditional statements as well.
Dershowitz and Manna [DM 75] discussed formalization of several programming
techniques involved in structured programming,
and demonstrated the use of these rules by hand-synthesizing programs.
Manna and Waldinger [MW 77c] have implemented such techniques in "DEDALUS", an
experimental program synthesis system. They have attempted to make life
easier for the user by simplifying the input required.
They have not, as yet, attempted to
describe completely their specification language; it is a superset of the
target language containing quantifiers and several high-level constructs
from the subject domain. Hundreds of transformation rules are available,
embodying a great deal of knowledge about the domain for which programs are to be
synthesized.
The transformations include rules for recursion formation,
conditional formation, and procedure formation. A goal given as input is
transformed into subgoals until a primitive program to accomplish it is
derived.
Strategic controls are used to choose among possible
synthesis paths.
Burstall and Darlington [BD 75] described a formal system for manipulation and
optimization of recursive functions. The language they use is that of
recursion equations. Darlington [D 75] extended this language to include
set notation (having been influenced by the work of Manna and Waldinger),
and described the application of the transformation system to the problem
of program synthesis. (The difference between program transformation and
program synthesis lies in the degree of abstraction in the specification
one starts with.) Non-trivial algorithms have been derived manually using
the transformation rules of the system, however cleverness is still needed
at some points to determine which rules to apply.
Clark and Sickel [CS 77] describe the process of deriving computational logic
programs (defined by Sickel [S 77a])
from axiomatic specifications. The process was investigated using
hand synthesis of programs, but an interactive system was intended to be
implemented that would become more automatic as the synthesis methodology
was refined. Clark and Darlington [CD 78] further this methodology using
a compromise notation of logic and recursion equations, making the
results applicable in both formalisms. They describe the synthesis of
recursive function definitions from axiomatic specifications. Sickel [S 77a]
also described a methodology for continuing the process down to an executable
form in a "conventional" programming language. By doing a theorem proving style
of analysis of the logic program one can derive a tree representing all possible
proofs of the program taken as a theorem. A regular expression is used to
describe a computation path representing all proofs of the theorem.
This computation path may then be mapped into a program in the target
programming language.
Observing that the structure of a program is often determined by the structure
of the data it operates on, von Henke [H 75] organized knowledge about the data
domain and represented it in such a way that it can directly assist a system
in constructing programs. He used LCF (Logic for Computable Functions),
extended to include terms for expressions involving sets and bounded quantification,
as the problem specification language. The fact that every LCF term also has
an interpretation as a computational rule for the function denoted by it allows
the term to be regarded as a program. Data type definitions are used to generate
"characterizing" functions (identity on the type defined and undefined elsewhere)
which can then be abstracted into functionals for homomorphic and endomorphic
extension. For instance, a predicate to recognize the type could be described
as a homomorphic extension into truth values. A function to accomplish
substitution, "replace free occurrences of %3v%1 in %3e%1 by %3t%1 after
renaming bound variables in %3e%1 so that no free variable in %3t%1 becomes
bound in the modified %3e%1", can be expressed as an endomorphism on the data type
"expressions".
All of the approaches mentioned above deal with formal systems in which the
proofs of equivalence of program and specification
can be carried out. Many researchers have experimented
with systems that automatically write or modify programs from partial
specifications in an ambiguous language (subsets of English), making correctness
more difficult to arrive at.
Heidorn [H 76] reviews four such projects that use natural language dialogues
with the machine for specification of the problem. Most such projects limit
the area of application severely. In his own research at the NPS (Naval Postgraduate
School, Monterey, Ca.) Heidorn used a restricted form of English as input
and generated GPSS programs as output. The system used hundreds of decoding and
encoding rules and was designed for generation of programs to do queueing
simulations. These it did well with the author of the system as user.
Another project aiming at natural language specification is being carried on
at the Information Sciences Institute of the University of Southern California.
This system, called SAFE [BGW 77], is intended to be independent of the problem
domain, and consists of three phases: "domain acquisition" [GBW 78], "planning"
[WBG 77], and a phase to produce the final program. The input to the system
is a (manually) parenthesized natural language program description retaining
most semantic ambiguities of natural language but avoiding its syntactic
ambiguities. The phases deal with the data and operation structure,
the program and control structure, and the program variable and
parameter structure, respectively.
Lenat [L 75] studied the problems involved in synthesizing large LISP
programs requiring several hours of user-system interaction time to generate
natural language specifications for the problem. The problem domain was
inductive inference programs. The system was made up of BEINGs,
experts on various topics (such as coding, probability, or contradiction),
capable of asking and answering questions of the user or other BEINGs.
It was found that to be successful a user had to be "familiar with LISP,
well-grounded in computer science, and have the input-output behavior
clearly in mind." The system was constructed with particular dialogues
in mind. Problems pointed out by the experiment were the inflexibility of
the system to new dialogues, its dependence on user reliability (no errors
allowed), and the system's inability to accept new high level domain-specific
knowledge (these additions had to be made through modifications of the
system itself).
Another approach is synthesis of programs by example. Hardy [H 75a] describes
a system that generates LISP functions from a single input-output pair.
He deals only in the domain of list-manipulating functions and claims that
"despite the fact that there are infinitely many functional extensions of the
input-output
.pt24
.begin center
(`iopair'): (A B C D) = > = ((A) (B) (C) (D))
.end
.pt24
there is only one function that would be regarded as the `obviously' intended
one." This is certainly true, and he has quite a few examples that work
as one might expect. However one can imagine several functions incapable of being
completely characterized by a single input-output pair, e.g., any function
which operates differently as the result of a test on the data it recieves as
an argument (if the first element of an integer list is even then ...).
Summers [S 77b] uses several sample input-output pairs to synthesize LISP
functions. This is acomplished by a series of transformations from a set
of examples to a program. Programs are synthesized in a subset of LISP
using the primitive functions %3car, cdr, cons,%1 and %3atom%1, and the
control structures of recursion, functional composition, and the conditional
expression.
The current system, THESYS, is able to derive programs with at most a single
recursive call. A technique called "differencing" is used to set up
equations that can be rewritten as a set of recurrence relations which are
then used to find the recursive program satisfying the examples. Another
technique, "variable addition", is used to generalize on a set of examples
with the hope of enabling differencing where it was not applicable before.
Rather than supply example input-output pairs, Ulrich and Moll [UM 77]
advocate supplying an entire program as an example and establishing an
analogy that the computer can use to derive another program. By extending
an analogy, a given program may be used to generate another program solving
a different but analogous problem. The analogy formation process works
with the proof of the known program rather than with its code. The proof
is attempted for the new domain and only altered when a step is not valid in
this domain. A change in the correctness proof causes a change in the code.
The initial analogy must always be specified by the user, making the solution
of subproblems somewhat awkward.
Biermann and Krishnaswamy [BK 76] construct programs from sample computation
traces. They have shown that if there exists a program capable of executing
the given trace, then their system will find that program (or one equivalent
to it). This approach assumes the user has an algorithm already in mind
(to supply the computation trace).
Several of the above approaches are brought to bear in a project lead by
Green [G 77] at Stanford University. The PSI program synthesis system
consists of two phases: an acquisition phase and a synthesis phase. The
specification is accomplished through a dialogue with the user, using
English descriptions, examples, and traces. The acquisition phase is
made up of a parser-interpreter, a trace and examples inference system, a
dialogue moderator, a domain expert, and a model builder. The synthesis
phase involves the interaction of a coder and an efficiency expert to
refine the program model into an efficient executable program. The PSI
system is being extended as the group attacks different problem domains.
.sec(Specification Language)
.turn on "↑↓&#"
.turn off "¬"
The input to the system is a sequence of definitions. A target definition
specifies the target language to be used, which may be changed during
a session by simply supplying another target definition.
The other kinds of definitions are function, type and generic.
A function definition has six parts, a name, an input pattern, a formal parameter
list, a precondition, a postcondition, and a body.
.begin nofill
.group
.fp
For example:
%3function Fact
input pattern? (1 0)
parameter list? (x y)
precond? Integer(x, true) ∧ ≥(x, 0, true).
postcond? Integer(y, true) ∧ >(y, 0, true).
body? Fact(0, 1)
Fact(z, w) ← Sub1(z, z1), Fact(z1, w1), *(z, w1, w).
.apart
.end
The verbosity in the indicators is endurable since the system
types out the question asking for each part of the specification following the
function name.
The name part is self-explanatory. An input pattern is a list of 1's and 0's
indicating which of the arguments of the function being defined are expected
to hold input values and which are used to carry values produced during the
computation of the function, respectively.
A formal parameter list is required to match up the appropriate arguments
for the precondition and postcondition specifications. As we will see,
the formal parameters are independent of the specification of the body.
The precondition is a well-formed-formula of predicate calculus,
defined on the input variables, that is true only
if the function is defined for those input variables.
By specifying precisely the domain of the function we can guarantee
termination of each program. The precondition is more than just a type declaration
in the usual sense, such as Integer or Real, it may also provide information
such as "%3x≥2%1" assuming that %3x%1 is an input variable.
Similarly, the postcondition is a predicate
formula on the output variables
that specifies the range of the output.
Taken together, the precondition and postcondition
specify the functionality, i.e. the domain and range, of the program being defined.
The range given may in fact be larger than the actual range of the function,
but the domain given must not include any extraneous elements.
A body definition is a set of Horn clauses that describes the function, usually
recursively, in an axiomatic way. Each Horn clause is an implication, stating
that the goal can be asserted if a set of subgoals can be satisfied. In writing
a body definition we are asserting that each of these implications is true.
.begin turn on "#"
Formally, a Horn clause is a disjunction of literals (atomic formulas, such as
"%3P(x, 2, y)%1", or negated atomic formulas) in which at most one literal is
positive (not negated). The implication form is derived from the fact that
%3(A ∨ ¬B ∨ ¬C) ≡ (A#←#B#∧#C)%1. There are four kinds of Horn clauses:
.end
.begin nofill
1) one with non-empty antecedent and consequent;
2) one in which the antecedent is empty and the consequent is non-empty;
3) a clause with non-empty antecedent and an empty consequent; and
4) an entirely empty clause.
.end
Only the first two
of these types of clauses are used in function definitions. The first is an
implication as mentioned above, the second is considered an assertion. (The
assertion arises from the fact that we can consider the form of the implication
to be a conjunction implying a disjunction, an empty conjunction is interpreted
as true, thus asserting the implication "%3true → A%1" is the same
as asserting "%3A%1".) Kowalski [K 74] describes the interpretation of Horn
clauses as a programming language. We will discuss the differences between
Logic programs and the specifications required by this system in a later
section; see {yon (p1)}.
A type definition is essentially a definition of the predicate that recognizes
occurrences of the type. In this sense it has the same form as any other function
definition.
The body of a type definition has the same form as that of a function definition.
For the sake of consistency, we require that each type predicate have an
output variable, just as any other function definition would. Although one may
not usually think of a predicate as needing an output variable, since the evaluation
of the predicate succeeds if and only if the answer is "true", the inclusion
of an explicit output variable allows us to distinguish when it is possible to
give an answer of "false" from the case in which we simply cannot determine that
the answer is "true".
.begin nofill
.group
.fp
.P11:
For example,
%3type Set
body? Set(Mt-set, true)
Set( Add-elem(y,X), true) ← Set(X, true), Member(y, X, false).%1
.apart
.end
Much of the information is implicit in a type definition. The
input pattern is always %3(1 0)%1, the formal parameter list is any list of two
variables, the precondition is %3TRUE%1,
and the postcondition is simply that the output variable ends up with
a truth value.
A generic function is one in which the input pattern is allowed to vary.
For example, one might wish to define a function "%3Concat(x, y, z)%1", meaning
"%3z%1 is the result of appending %3x%1 and %3y%1". If defined as a generic
function we can use %3Concat%1 in defining other functions whenever we
have two of its arguments available and wish to compute the third.
The definition of a generic
function includes its name, a formal parameter
list (again for the purposes of the preconditions and postconditions), a
list of choices specifying how the function may be used, and possibly
more than one body definition.
.begin nofill;turn on "↑"
.fp
The general form of a generic specification is⊗↓The subscripts used are for clarity
in the example; they are not part of the syntax.←:
%3"generic" name
"parameter list?" id-list
"choices?"
input-pattern%41%3
"function name?" funname%41%3
"precond?" precondition%41%3
"postcond?" postcondition%41%3
"body-name?" bodyname%41%3
. . .
input-pattern%4n%3
"function name?" funname%4n%3
"precond?" precondition%4n%3
"postcond?" postcondition%4n%3
"body-name?" bodyname%4n%3 "."
"body-defs:"
name%41%3 "?" h-clause%41%3↑* "."
. . .
name%4k%3 "?" h-clause%4k%3↑* "." %1
.end
A choice is made up of an input pattern, a name to be associated with this
particular style of call on the function, domain and range specifications, and a
body name indicating the function body to be used.
A body definition
associates a body name with a definition (i.e. a set of Horn clauses).
.ss(Syntax of the Specification Language)
.P3:
A context-free description of the input language is as follows:
.begin "bnf" nofill; select 3;turn on "↑";single space;
.fp
%1PHRASE STRUCTURE:%3
.pt24
input ::= definition↑* "."
.pt18
definition ::= fun-def | type-def | gen-def | target-def
.pt18
fun-def ::= "function" name
"input pattern?" input-pattern
"parameter list?" id-list
"precond?" precondition
"postcond?" postcondition
"body?" h-clause↑* "."
.pt18
type-def ::= "type" name
"body?" h-clause↑* "."
.pt18
gen-def ::= "generic" name
"parameter list?" id-list
"choices?" %2[%3choice "choices?"%2]%3↑* "."
"body-defs:" body-def↑*
.pt18
target-def ::= "target" target-language
.pt18
target-language ::= name
.pt18
choice ::= input-pattern
"function name?" name
"precond?" precondition
"postcond?" postcondition
"body-name?" name
.pt18
body-def ::= name "?" h-clause↑* "."
.pt18
input-pattern ::= "(" zero-or-one↑* ")"
.pt18
zero-or-one ::= "0" | "1"
.pt18
name ::= identifier
.pt18
id-list ::= "(" name↑* ")"
.pt18
precondition ::= disjunction "."
.pt18
postcondition ::= disjunction "."
.pt18
disjunction ::= conjunction | conjunction "∨" disjunction
.pt18
conjunction ::= literal | literal "∧" conjunction
.pt18
literal ::= "True" | "T" | pred-app | "(" disjunction ")"
.pt18
pred-app ::= name arglist
.pt18
arglist ::= "(" arg↑* ")"
.pt18
arg ::= fun-app | variable | constant
.pt18
fun-app ::= name arglist
.pt18
variable ::= identifier
.pt18
h-clause ::= goal "←" subgoals | goal
.pt18
goal ::= pred-app
.pt18
subgoals ::= pred-app %2[%3 "," pred-app%2]%3↑*
.pt18
constant ::= number | string | "true" | "t" | "false" | "f"
| "undef" | "(" ")" | quoted-const
.pt18
string ::= dblquote %2[%3 anychar | punctuation | dblquote dblquote | " " %2]%3↑* dblquote
.pt18
punctuation ::= "," | "." | "'" | "`" | ";" | ":" | "[" | "]" | "(" | ")"
.pt18
variable ::= identifier
.pt18
quoted-const ::= "'" exp
.pt18
exp ::= identifier | "(" elem↑* ")"
.pt18
elem ::= constant | variable | exp
.next page
.fp
%1LEXICON:
.pt18
number ::= integer | real
.pt18
integer ::= digit-seq | sign digit-seq
.pt18
mantissa ::= integer "." digit↑* | sign "." digit-seq | "." digit-seq
.pt18
real ::= mantissa | mantissa "e" integer
.pt18
digit-seq ::= digit digit↑*
.pt18
digit ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
.pt18
sign ::= "+" | "-"
.pt18
%3identifier ::= anychar | anychar identifier
.turn off "{}"
.pt18
%1where %3anychar ε {≡,%1∩%3,∪,⊂,⊃,∩,+,-,*,&,//,≤,≥,<,>,≠,=,α,β,ε,λ,π,∀,∃,!,?,
q,w,e,r,t,y,u,i,o,p,a,s,d,f,g,h,j,k,l,z,x,c,v,b,n,m,Q,
W,E,R,T,Y,U,I,O,P,A,S,D,F,G,H,J,K,L,Z,X,C,V,B,N,M}
.pt18
%1and%3 dblquote ε { " }
.turn on "{}"
.end "bnf"
.ss(Semantics of the Specification Language)
.P2:
%1The semantics of a function specification:
.begin "spec" nofill;select 3;turn on "↑"
"function" name
"input pattern?" input-pattern
"parameter list?" id-list
"precond?" precondition
"postcond?" postcondition
"body?" h-clause↑* "."
.end "spec"
.fp
informally, is that for all
possible instantiations of the formal parameter list, if each parameter
designated as an input by the input pattern has a value bound to it and
the value of the precondition evaluated on the inputs is true (i.e., the
inputs lie within the domain of definition of the function), then the
conjunction of each of the Horn clauses and the postcondition is true.
Expressed as a formula in first order logic:
.begin "form" nofill
.turn on "↑"
%2∀%g¬%2x defined[ inputs[S[%3id-list%2], S[%3input-pattern%2]] ] ∧ S[%3precondition%2] →
S[%3h-clause↑*%2] ∧ ((S[%3name%2] S[%3id-list%2]) → S[%3postcondition%2])%1⊗↓We assume
that the logical operators have the following precedence relationships, from
tightest to least binding: ¬, ∧ and ∨, →, ≡ or <->.←
where:
.p10:
the semantic function %2S%1 maps elements of the specification language onto their
denotations in first-order logic. Due to the similarity of the languages
involved, this mapping is the identity mapping for the %3id-list, input-
pattern, %1and %3name%1. The denotations of the %3precondition%1 and %3postcondition%1
are the obvious formulas of first-order logic. Elements of the semantic
domain will be given in bold type whenever a distinction is desired.
%g¬%2x%1 represents all variables in %2S[%3id-list%2]
%2inputs[S[%3id-list%2], S[%3input-pattern%2]]%1 is the list of input parameters, i.e., those
parameters in %2S[%3id-list%2]%1 corresponding to 1's in %2S[%3input-pattern%2]
%2defined[u]%1 is true iff every element of the list %2u%1 has a value that is
completely defined (contains no free variables)
%2S[%3h-clause↑*%2]%1 is the conjunction of the semantics of the individual horn
clauses. The semantics of each horn-clause is that for all variables
mentioned, the conjunction of the right-hand-side implies the
left-hand-side.
S[%3name id-list%2]%1 is the denotation of the application of %2S[%3name%2]%1 to %2S[%3id-list%2]%1 in
first-order logic.
.group
.fp
For example:
%3function Fact
input pattern? (1 0)
parameter list? (x y)
precond? Integer(x, true) ∧ ≥(x, 0, true).
postcond? Integer(y, true) ∧ >(y, 0, true).
body? Fact(0, 1)
Fact(z, w) ← Sub1(z, z1), Fact(z1, w1), *(z, w1, w).
.apart
.fp
%1has the semantics of the associated first order logic expression:
%2∀x,y [ defined[(x)] ∧ Integer(x, true) ∧ ≥(x, 0, true) →
Fact(0, 1)
∧ ∀z,z1,w,w1 [ [Sub1(z, z1) ∧ Fact(z1, w1) ∧ *(z, w1, w) → Fact(z, w)] ]
∧ [ Fact(x, y) → Integer(y, true) ∧ >(y, 0, true) ] ]
.end "form"
%1The semantics of a type specification:
.begin "spec2" nofill; select 3;turn on "↑"
"type" name
"body?" h-clause↑* "."
.end "spec2"
.fp
%1 is given by the first order logic formula:
.begin "form2" nofill;turn on "↑"
%2∀x defined[ (x) ] → %2S[%3h-clause↑*%2]
∧ [ S[%3name (x, y)%2] → boolean(y,true)]
.end "form2"
.fp
%1The antecedent of the implication guarantees that we have an input value,
the consequent asserts the conjunction of the Horn
clauses making up its body and the fact that the result of a type predicate
is a truth value. The precondition is "%2True%1" (and therefore need not even
appear in the antecedent of the implication) since we want to allow anything
at all as input to a type predicate, the postcondition need not be stated explicitly
in the specification since it is always the same.
The semantics of a generic function specification⊗↓Note again that the subscripts
are not part of the syntax←:
.begin "spec3" nofill; select 3
.turn off "{,}";turn on "↑"
"generic" name
"parameter list?" id-list
"choices?"
input-pattern%41%3
"function name?" funname%41%3
"precond?" precondition%41%3
"postcond?" postcondition%41%3
"body-name?" bodyname%41%3
. . .
input-pattern%4n%3
"function name?" funname%4n%3
"precond?" precondition%4n%3
"postcond?" postcondition%4n%3
"body-name?" bodyname%4n%3 "."
"body-defs:"
name%41%3 "?" h-clause↑*%41%3 "."
. . .
name%4k%3 "?" h-clause↑*%4k%3 "."
.fp
%1is given by the conjunction:
%9∧%6↑n&↓i↓=↓1 %2∀%g¬%2x [ (S[%3funname%4i%3 id-list%2] → S[%3name id-list%2]) ∧
(defined[ inputs[S[%3id-list%2], S[%3input-pattern%4i%2]] ] ∧ S[%3precondition%4i%2] →
%2S[ H-C[%3bodyname%4i%2] ] ∧ (S[%3funname%4i%3 id-list%2] → S[%3postcondition%4i%2]) ) ]%1
.group
where:
H-C[%3bodyname%4i%2] %1 is the %3h-clause↑*%4j%1 associated with %3bodyname%4i%1,
the %3input-pattern%4i%1's are distinct,
the %3funname%4i%1's are distinct,
the %3bodyname%4i%1's need not be distinct,
the %3name%4j%1's are all distinct and are all the different %3bodyname%4i%1's listed above,
and %2S%1 is the identity mapping on %3bodyname%1's and %3funname%1's.
.apart
.end "spec3"
Thus the generic specification has the effect of defining several diferent functions
and associating them all with a "generic" name that can be used when one does
not wish to bother with using a different name every time the function is called in
a different way, that is, with a different input-pattern.
The semantics of a target definition is simply the ordinary Hoare rule for
assignment:
.begin nofill;turn off "{,}"
%2P[name/target] { %3target name%2 } P %1
.end
Using this specification language we can describe an algorithm for unification
of two lists of terms as follows:
.begin nofill;select 3
function Unify
input pattern? (1 1 0)
parameter list? (t1 t2 s)
precondition? List(t1, true) ∧ List(t2, true).
postcondition? Substitution(s, true).
body? Unify( (), (), ())
Unify( (), cons(x,u), undef)
Unify(cons(x,u), (), undef)
Unify(cons(x,t1), cons(y,t2), s) ← Unifyterms(x, y, s1),
Mk-subst(s1, t1, t2, newt1, newt2),
Unify(newt1, newt2, s2),
Compose-subs(s1, s2, s).
.end
.sec(Logic Programming versus Synthesis,,,P16:)
.p1:
Predicate logic can be viewed as a powerful, high level, nondeterministic programming
language. Why not simply program in logic instead of bothering with a system
to obtain programs in some other language? For one thing, logic is often more
powerful than we need, and this power is not free. The full backtracking
abilities required by an implementation of logic can be costly in time
and space. Also, some languages are better suited to particular
problems than are others. Although the style of program generated by the
system proposed here is inherited from the specification and
therefore similar in all languages,
a program transformation system may be constructed that could optimize programs
in a specific language to take advantage of its special features. The main
purpose of the synthesis system is to see that we end up with correct programs.
In this section we look at logic as a programming language, and then as part of
the specification language for this system.
The completeness of the Horn clause subset of predicate logic as a programming
language has been proven by Andreka and Nemeti [AN 76]. The operational semantics
has been found [EK 74] to be part of the proof theory of predicate calculus and
thus closely related to the axiomatic semantics. The operational semantics
involves consideration of all possible derivations from the axioms. This implies,
among other things, the ability to compute relations, not just functions. For
example, the operational semantics of the atomic formula %3Times(x,#y,#z)%1,
would be described as follows:
.begin center;turn off "{}";turn on "↓"
%3(a, b, c) %2ε D%4op%2[%3Times%2] iff %3(a, b, c)%2 ε { %3(x, y, z) | %br%g↓~%2↓A %3 Times(x, y, z)%2}
.end
.fp
where %g~%2A%1 is the theory of predicate calculus
augmented by the definitions given as axioms. A computation of %3Times(3, 4, x)%1
would find only one answer, with %3x%1=12. However, a computation of %3Times(x, y, 12)%1
would involve several derivations: %3Times(1, 12, 12)%1, %3Times(12, 1, 12)%1,
%3Times(2, 6, 12)%1, %3Times(6, 2, 12)%1, %3Times(3, 4, 12)%1, and
%3Times(4, 3, 12)%1, (in some order). The computation
of %3Times(3, y, z)%1 would never terminate since there are an infinte number
of derivations possible.
There is no distinction made between input and output. A given tuple is in a
particular relation or not. This facet of logic programming is particularly
useful in data base applications [E 78].
There is no order of evaluation implied by a logic program. Its operational
semantics involve %2all%1 derivations without indicating which should be attempted
first. Thus, a logic program, together with a call on it, determines a computation
tree but says nothing of which path to follow. Under these circumstances,
to prove termination of a logic program, one must prove the tree is finite.
In any given implementation of a logic interpreter things are not that bad.
The order of evaluation is deterministic, so the tree is always traversed in a
predictable way. Even so, if all derivations are to be attempted, termination
occurs only for finite trees. However, termination can be proved under some
circumstances.. For example, if only a single answer rather than %3all%1 answers
is desired, then one may be able to prove termination for a particular order of
evaluation with respect to specific argument positions being designated for inputs.
In the current system we have chosen to define functions rather than relations,
in the sense that we want a single unique answer to a question rather than all
possible answers. This decision is based on the belief that a programmer knows
when %3the%1 answer, %3any%1 answer, or %3all%1 answers to a problem is desired
and can design the program to ask for such explicitly. Asking for the
answer "the set of all
framices that foo" is a request for a single unique answer.
The specification of a function includes a Horn clause description. The
specification is translated into a deterministic algorithm expressed in
an intermediate language. Currently,
clauses are tried in the order given as are subgoals within a clause. An
automatic ordering is under consideration by Mike Franusich at the University of
California at Santa Cruz.
Some analysis can be done to ensure, for example, that termination cases are
attempted first, and subgoals that produce values are called before other subgoals
that need those values as input.
We distinguish between input and output variables for two reasons. First,
given which values are expected to be available and which are to be computed,
we can often prove termination when in the general case we may not be able to
(for instance, in the %3Times(x, y, z)%1 example discussed earlier). Also, perhaps
more importantly, we believe that programs tend to be based on the construction of
the variables one expects to compute. The programmer is more likely to see a
task as deriving output information from given input information than as a
non-directional exploration of the relationship between the two. Thus, even if
the program terminates when inputs and outputs are interchanged, the computation
may become horribly inefficient.
Programs can be written that are "nicely" invertible, meaning that one direction
of computation is about as efficient as another.
In logic programs invertibility is more general than simply swapping of input and
output variables; we are dealing with n-tuples not ordered pairs. Thus, for an
n-ary predicate there are 2%8n%1 different ways of designating input and output
variables. Sickel [S 78] describes j-invertibility, refering to the jth variable
of the n-tuple. She presents some guidelines for constructing invertible functions,
and describes algorithms to test the invertibility of programs.
Since it can often be useful to describe one procedure that may be used in different
ways, we have included the concept of a "generic function"⊗↓According to the
dictionary, "generic" means
"applicable or referring to all the members of a genus or class". A "generic"
function is mentioned elsewhere in the literature as a function whose specific form
is determined by the data type of its arguments. We are extending this notion to
include functions whose "input patterns" (determining which formal parameters
are to be expected as input when a function is called) may vary.
The implementation of the generic
chosen by type rather than input pattern is suggested as an extension of the current
system .←.
We wish to allow the
convenience of invertible functions while requiring the programmer to be aware of
the possibilities in the program. Thus, we require that one list the different
calling styles by input-pattern and indicate a function body (set of Horn clauses)
to be used in each case. A predicate with six different (useful) calling styles
may use the same logic program as the specification for three input-patterns,
another for two input-patterns, and a third for the last. Thus we get the best
of both worlds; we know enough to maintain the guarantee of termination, and the
user gains the flexibility afforded by a generic function in the specification of
other programs. The system attaches a different name to each function body and
determines from context which is appropriate in a given instance of the generic.
.sec(Intermediate Language)
The intermediate language form of function definitions is strictly for use
by the system. The user never sees or programs anything in the internal form.
The auxiliary specifications (all but body specifications) are essentially
unchanged; their representation is slightly different but exactly the same
information is expressed. Thus, the only really interesting part of the
intermediate form is its treatment of the body specification.
The body of a function in internal form is a "backtracking-conditional" ("bktrkcond"
for short).
The name is slightly too general as only a restricted, well behaved, kind
of backtracking is allowed.
Each clause of the specification becomes an "alternative" in the bktrkcond. An
alternative consists of a "match"-part, which is
an argument list to be matched against the actual
parameters of a function call, and a "try" part consisting of the subgoals
to be accomplished.
If the match-part of an alternative is accomplished, then the actual call on the
function is an instantiation of the head (or goal) part of the clause from which
the alternative was derived. Thus, according to the specifications, we can assert
this call if it is possible to accomplish all the subgoals. If the match-part
succeeds then we attempt the try-part of the alternative. If the try-part is
successful, then we are done; if not, then we must look for another alternative.
The backtracking involved is well-behaved in the sense that we backtrack only
over entire alternatives, never over individual subgoals in the try-part of an
alternative. All that must be undone is the bindings made in accomplishing
the unification of the actual parameter list with the argument list in the
match-part of the alternative.
We impose determinism on the program at this stage by insisting on a particular
order for considering the alternatives: the order in
which the user supplied them to the system. An extension to the system
is desired that would analyze the alternatives
and decide for itself what order would be most effective. The ordering of the
subgoals is also open to question. These issues are being investigated
by M. Franusich, a student at UCSC, and we hope to incorporate his results
eventually.
The intermediate form of a generic specification involves two things.
First, the intermediate form of a generic definition contains only
the parameter list of the function and a list associating input-patterns
with the function name to be used when that input-pattern is recognized. Although
it does not appear in the internal generic definition, a generic specification
causes the function definitions for each alternative version of the function
to be made.
The Intermediate Language is similar to the Input Language in many ways.
To point out the similarities, we have used the same nonterminal names
where applicable. All the nonterminals are prefixed with a "$" to distinguish them
from those of the Input Language.
.ss(Syntax of Intermediate Language)
.P4:
A context-free grammar describing the Intermediate Language is:
.begin "bnf" nofill; select 3;turn on"↑";single space
.fp
%1PHRASE STRUCTURE:%3
.pt24
program ::= $definition↑*
.pt18
$definition ::= $fun-def | $type-def | $gen-def | $target-def
.pt18
$fun-def ::= "(" "function" $name $input-pattern $id-list
$precondition $postcondition $body ")"
.pt18
$type-def ::= "(" "type" $name "(1 0)" "(x y)" "T" "(boolean y)" $body ")"
.pt18
$gen-def ::= "(" "generic" $name $id-list $selection↑* ")"
.pt18
$target-def ::= "(" "setq" "target" $target-language ")"
.pt18
$target-language ::= $name
.pt18
$selection ::= $input-pattern $name
.pt18
$input-pattern ::= "(" $zero-or-one↑* ")"
.pt18
$zero-or-one ::= "0" | "1"
.pt18
$name ::= $identifier
.pt18
$id-list ::= "(" name↑* ")"
.pt18
$precondition ::= $disjunction
.pt18
$postcondition ::= $disjunction
.pt18
$disjunction ::= $conjunction | "(" "∨" $conjunction $disjunction ")"
.pt18
$conjunction ::= $literal | "(" "∧" $literal $conjunction ")"
.pt18
$literal ::= "T" | $pred-app | $disjunction
.pt18
$pred-app ::= "(" $name $arg↑* ")"
.pt18
$body ::= $backtracking-conditional
.pt18
$backtracking-conditional ::= "(" "bktrkcond" $alternatives ")"
.pt18
$alternatives ::= $match-try-pair↑*
.pt18
$match-try-pair ::= "(" $arglist "(" "try" $subgoals ")" ")"
.pt18
$arglist ::= "(" $arg↑* ")"
.pt18
$arg ::= $fun-app | $variable | $constant
.pt18
$fun-app ::= "(" $name $arg↑* ")"
.pt18
$subgoals ::= $pred-app↑*
.pt18
$variable ::= identifier
.pt18
$constant ::= number | $string | "true" | "false" | "undef" | "(" ")" | $quoted-const
.pt18
$string ::= "(" "string" $char-list ")"
.pt18
$char-list ::= "(" %2[ %3anychar | $punctuation | dblquote | " " %2]%3↑* ")"
.pt18
$punctuation ::= "," | "/." | "`" | "/'" | ";" | ":" | "/[" | "/]" | "/(" | "/)"
.pt18
$quoted-const ::= "(" "quote" $exp ")"
.pt18
$exp ::= identifier | "(" $elem↑* ")"
.pt18
$elem ::= $constant | $variable | $exp
.pt24
.fp
%1The LEXICON is the same as for the specification language.
.end "bnf"
.ss(Semantics of the Intermediate Language)
.P5:
The semantics of the intermediate language form of a function definition:
.begin verbatim; select 3
$fun-def ::= "(" "function" $name $input-pattern $id-list $precondition
$postcondition $body ")"
.end
.fp
is given by the first order logic formula:
.begin "spec4" nofill
%2∀%g¬%2x defined[ inputs[S[%3$id-list%2], S[%3$input-pattern%2]] ] ∧ S[%3$precondition%2] →
S[%3$body%2] ∧ (S[%3$name $id-list%2] → S[%3$postcondition%2])%1
where:
the semantic function %2S%1 maps elements of the intermediate language onto their
denotations in first-order logic. This is the obvious mapping for %3$id-list,
$input-pattern, $name, $precondition, %1and%3 $postcondition.%1 (see {yon (p10)}
%g¬%2x%1 represents all variables in %2S[%3$id-list%2]%1
%2inputs[S[%3$id-list%2], S[%3$input-pattern%2]]%1 is the list of input parameters, i.e.,
those parameters in %2S[%3$id-list%2]%1 corresponding to 1's in %2S[%3$input-pattern%2]%1
%2defined[l]%1 is true iff every element of the list %2l%1 has a value that is
completely defined (contains no free variables)
and the semantics of the function body %2S[%3$body%2]%1 is given below.
.fp
The intermediate form of a function body is:
%3 "(" "bktrkcond" "(" $arglist%41%3 "(" "try" $subgoals%41%3 ")" ")"
. . .
"(" $arglist%4n%3 "(" "try" $subgoals%4n%3 ")" ")" ")"
.end "spec4"
Informally, the semantics can be expressed as a conjunction of implications each of
which states that if the values bound to the %3$id-list%1 are an
instantiation of %3$arglist%4i%1 then the conjunction of all the subgoals in
%3$subgoals%4i%1 implies %3($name $arglist%4i%3)%1. Of course any substitutions
necessary to unify the %3$id-list%1 and %3$arglist%4i%1 must
be made throughout the %3$subgoals%4i%1.
We actually want an "ordered" conjunction, to ensure that the implications
involved in each alternative are considered in the order given. We want to
say that if both antecedents in the implication are true then we can
successfully claim the consequent and do not wish to consider the remaining
implications as applicable; however, if either antecedent is false, then we want
to proceed looking for an implication that is "useful" to us.
Let us represent by %7s%4i%1 the substitution applied to unify⊗↓Unification is the
process of finding a "most general substitution", in the sense of making
as few bindings as possible, which will render the objects being unified
to be syntactically identical. See [D 76], or [M 64] for a complete definition.←
%3$arglist%4i%1
with %3$id-list%1, if such a unification is possible.
For all A, A%7s%4i%1 is A with all substitutions in %7s%4i%1 made.
.group
Expressed as a formula of first order logic:
.begin nofill
.turn off "{}∞⊗";turn on "⊗" for "["; turn on "∞" for "]";turn on "#"
%9∧%6↑n&↓i↓=↓1%2 [ (unify[S[%3$id-list%2], S[%3$arglist%4i%2]] = %7s%4i%2) ∧ %9∧%6↑⊗i-1∞&↓⊗#j=1∞%2#(¬b%4j%2) →
( %2S[%3$subgoals%4i%7s%4i%2] → S[%3$name $arglist%4i%2]%7s%4i%2 ) ]
.apart
.group
%1where:
%2S%1 is again obvious on %3$arglist%1's and %3$subgoals%1's
%2b%4j%1 stands for %2(unify[S[%3$id-list%2], S[%3$arglist%4j%2]] = %7s%4j%2) ∧ S[%3$subgoals%4j%7s%4j%2]%1
%2S[%3$subgoals%4i%7s%4i%2]%1 is the conjunction of all subgoals in %3$subgoals%4i%1
with the substitution %7s%4i%1 made throughout,
and all free variables are universally quantified.
.apart
.end
The semantics of a type definition is, again, very similar to that of a function
definition. The semantics of the type definition:
.begin "type" nofill; select 3;
"(" "type" $name "(1 0)" "(x y)" "T" "(boolean y)" $body ")"
.fp
%1is given by the formula:
%2∀x defined[ (x) ] → S[%3$body%2] ∧ ((S[%3$name (x y)%2]) → S[%3(boolean y)%2])%1
where %2S[%3$body%2]%1 is as defined above for function bodies.
.end "type"
The semantics of a generic definition:
.begin "gen" nofill; select 3
"(" "generic" $name $id-list
$input-pattern↓1 $name↓1
. . .
$input-pattern↓n $name↓n ")"
.end "gen"
.fp
is given through an association of a call on %3$name%1 with the %3$name↓i%1
determined by the positions of the arguments having values at
the time the function is called. Formally:
.begin "gen2" nofill
.turn off "{, }"
%9∧%6↑n&↓i↓=↓1%2 ∀%g%2x [
S[def-of[%3$name%4i%2]] ∧ (S[%3$name%4i%3 $id-list%2] → S[%3$name $id-list%2]) ]
%1where: %2S[def-of[%3$name%4i%2]]%1 is the semantics of the function definition of %3$name%4i%1.
i.e.,
%2∀%g¬%2x defined[ inputs[S[%3$id-list%2], S[%3$input-pattern%4i%2]] ]
∧ S[%3$precondition%4i%2] →
S[body-of[%3$name%4i%2]] ∧ (S[%3$name%4i%3 $id-list%2] → S[%3$postcondition%4i%2])%1
The semantics of a target definition:
%3"(" "setq" "target" $name ")"
%1 is the Hoare rule for assignment:
%2P[%3$name/target%2] {%3 (setq target $name) %2} P
.end "gen2"
.sec(Mapping From Input Specification to Intermediate Form)
We now define the mapping %dI%1 (for "internalize") from input specifications
into intermediate language. In the first column we identify the input form
being translated, the center column shows the translation, and the third column
relates nonterminals of the input language to the instance being translated.
Since the lexicon for both languages is the same, the translation is concerned
only with the phrase structure of the languages.
.begin "ispec" nofill;turn on "↑";tabit2(20,60)
%dI%1[%3input%1] = \%dI%1[%3definition↑*%1]\%3input=definition↑*
%dI%1[%7e%1] =\%7e%1\where %7e%1 is the empty string
%dI%1[%3definition%41%3 definition↑*%1] =
\%dI%1[%3definition%41%1] %dI%1[%3definition↑*%1]
%dI%1[%3definition%1] =\%dI%1[%3fun-def%1]\%3definition = fun-def
%dI%1[%3definition%1] =\%dI%1[%3type-def%1]\%3definition = type-def
%dI%1[%3definition%1] =\%dI%1[%3gen-def%1]\%3definition = gen-def
%dI%1[%3definition%1] =\%dI%1[%3target-def%1]\%3definition = target-def
%dI%1[%3fun-def%1] =\%3"( function" name input-pattern\fun-def="function" name
\id-list %dI%1[%3precondition%1]\%3 "input pattern?" input-pattern
\%dI%1[%3postcondition%1]%3 "(" "bktrkcond" \ "parameter list?" id-list
\ %dI%1[%3h-clause↑*%1]%3 ")" ")"\ "precond?" precondition
\\ "postcond?" postcondition
\\ "body?" h-clause↑* "."
.end "ispec"
%1The function %dI%1 is the identity mapping on %3name%1's, %3id-list%1's, and
%3input-pattern%1's, and on %3precondition%1's and %3postcondition%1's it
is simply a translation to a fully parenthesized prefix form of representation.
.begin "ispec2" nofill;turnon "↑";tabit2(25,58)
%dI%1[%3precondition%1] =\%dI%1[%3disjunction%1]\%3precondition = disjunction "."
%dI%1[%3postcondition%1] =\%dI%1[%3disjunction%1]\%3postcondition = disjunction "."
%dI%1[%3disjunction%1] =\%dI%1[%3conjunction%1]%3\disjunction = conjunction
%dI%1[%3disjunction%1] =\%3"( ∨" %dI%1[%3conjunction%1]\%3disjunction =
\ %dI%1[%3disjunction%1]%3 ")"\ conjunction "∨" disjunction
%dI%1[%3conjunction%1] =\%dI%1[%3literal%1]\%3conjunction = literal
%dI%1[%3conjunction%1] =\ %3"( ∧" %dI%1[%3literal%1]\%3conjunction =
\ %dI%1[%3conjunction%1] %3")"\ literal "∧" conjunction
%dI%1[%3literal%1] =\%3"T"\literal = "TRUE"
%dI%1[%3literal%1] =\%3"T"\literal = "T"
%dI%1[%3literal%1] =\%dI%1[%3pred-app%1]%3\literal = pred-app
%dI%1[%3literal%1] =\%dI%1[%3disjunction%1]\%3literal = "(" disjunction ")"
%dI%1[%3pred-app%1] =\%dI%1[%3name arglist%1]\%3pred-app = fname⊗↓%1The internalized
form of a generic application will have a different name substituted for
the name of the generic if it appears in the specification of the body of a
function. This is why we listed %3name%1 as the translate of %3fname%1 above.
The name which is chosen will depend on the input pattern of the function
being specified.←arglist
%dI%1[%3name arglist%1] =\%3"(" name %dI%1[%3arg↑*%1] %3")"\arglist = "(" arg↑* ")"
%dI%1[%3arg%41%3 arg↑*%1] =\%dI%1[%3arg%41%1] %dI%1[%3arg↑*%1]
%dI%1[%3arg%1] =\%dI%1[%3constant%1]\%3arg = %3constant
%dI%1[%3arg%1] =\%3variable\arg = variable
%dI%1[%3arg%1] =\%dI%1[%3fun-app%1]\%3arg = fun-app
%dI%1[%3constant%1] =\%3number\constant = number
%dI%1[%3constant%1] =\%3"(" "string" %dI%1[%3string%1]%3 ")"\constant = string
%dI%1[%3constant%1] =\%3"true"\constant = "true"
%dI%1[%3constant%1] =\%3"true"\constant = "t"
%dI%1[%3constant%1] =\%3"false"\constant = "false"
%dI%1[%3constant%1] =\%3"false"\constant = "f"
%dI%1[%3constant%1] =\%3"undef"\constant = "undef"
%dI%1[%3constant%1] =\%3"(" ")"\constant = "(" ")"
%dI%1[%3constant%1] =\%dI%1[%3quoted-const%1]\%3constant = quoted-const
%dI%1[%3fun-app%1] =\%dI%1[%3name arglist%1]\%3fun-app = name arglist
%dI%1[%3string%1] =\%3"(" "string"\string = dblquote
\%dI%1[ [%3anychar | punctuation\%1[%3anychar | punctuation
\| dblquote dblquote | " "%1]%3↑*%1 ] %3")"\ | dblquote dblquote
\\ | " "%1]%3↑* dblquote
%dI%1[ [%3anychar | punctuation
| dblquote dblquote | " "%1]%3↑*%1 ] =
"(" [ %dI%1[%3anychar%1]
| %dI%1[%3punctuation%1]
| %dI%1[%3dblquote dblquote%1]
| %dI%1[%3" "%1] ]%3↑* ")"
%dI%1[%3anychar%1] =\%3anychar
%dI%1[%3punctuation%1] =\%3punctuation\punctuation =
\\"," | "." | "`"
\\| "'" | ";" | ":"
%dI%1[%3dblquote dblquote%1] =\%3dblquote
%dI%1[%3" "%1] =\%3"/ "
%dI%1[%3quoted-const%1] =\%3"(" "quote" %dI%1[%3exp%1] %3")"\quoted-const = "'" exp
%dI%1[%3exp%1] =\%3identifier\exp = identifier
%dI%1[%3exp%1] =\%3"(" %dI%1[%3elem↑*%1] %3")"\exp = "(" elem↑* ")"
%dI%1[%3elem%41%3 elem↑*%1] =\%dI%1[%3elem%41%1] %dI%1[%3elem↑*%1]
%dI%1[%3elem%1] =\%dI%1[%3constant%1]\%3elem = constant
%dI%1[%3elem%1] =\%dI%1[%3variable%1]\%3elem = variable
%dI%1[%3elem%1] =\%dI%1[%3exp%1]\%3elem = exp
%dI%1[%3variable%1] =\%3identifier\variable = identifier
%dI%1[%3variable%1] =\%3!identifier\variable = identifier
\\%1formal parameters are
\\indicated by a first
\\character "!"
.end "ispec2"
The interesting part of %dI%1 maps Horn clauses onto the intermediate
form of the function body.
Whenever an instance of a
generic call is encountered in the body of a specification, the first version
of the generic whose input pattern is satisfied, i.e. all argument positions
corresponding to 1's in the input pattern have values supplied, is substituted
for the generic. Thus we never have to translate generic specifications into
the target language; we just translate each specific version.
.begin "spec3" nofill;turn on "↑";tabit2(20,60)
%dI%1[%3h-clause%41%3 h-clause↑*%1] = %dI%1[%3h-clause%41%1] %dI%1[%3h-clause↑*%1]
%dI%1[%3h-clause%1] =\%dI%1[%3goal%1] \%3h-clause = goal
%dI%1[%3goal%1] =\%3"(" arglist "(" "try" ")" ")"\goal = pred-app
\\ = name arglist
%dI%1[%3h-clause%1] =\%3"(" arglist \%3h-clause = goal "←" subgoals
\ "(" "try" %dI%1[%3subgoals%1] %3")" ")"\ goal = name arglist
%dI%1[%3subgoals%1] =\%dI%1[%3pred-app%41%1] \%3subgoals =
\ %dI%1[[%3"," pred-app%1]%3↑*%1]\%3 pred-app%41%1 [%3 "," pred-app%1]%3↑*
%dI%1[%3"," pred-app%41%3
%1[%3"," pred-app%1]%3↑*%1] = %dI%1[%3pred-app%41%1] %dI%1[[%3"," pred-app%1]%3↑*%1]
.end "spec3"
For type specifications we have:
.begin "spec4" nofill;tabit2(20,60);turn on "↑"
%dI%1[type-def%1] =\%3"(" "type" name "(1 0)" \type-def =
\"(x y)" "T" "(boolean y t)" \ "type" name
\"(" "bktrkcond" %dI%1[%3h-clause↑*%1]%3 ")"\ "body?" h-clause↑* "."
.end "spec4"
As discussed earlier, one may consider the type definition to be the definition
of a predicate to recognize instances of the type. We must make a distinction
between a type definition and the recognizer for a type when our target
language is strongly typed. This will be discussed in the mapping from
intermediate form to target language.
The mapping from the input specification of a generic function to its intermediate
form involves not only the internal form of the generic definition but also that
of each of the specific versions of the generic being defined. The function
%dSelect%1 creates a sequence of %3input-pattern fname%1 pairs from which the
choices of individual functions to substitute for generic calls will be made.
The function %dMake-defs%1 creates a function definition for each version of the
generic. The resulting definitions are identical to those that would have
been created if each version were specified explicitly as a %3fun-def%1.⊗↓The
variables %3gname, fname%1, and %3bname%1, in the following, are all instances
of the nonterminal %3name%1.←
.begin "spec5" nofill; turn on "↑";tabit2(20,60)
%dI%1[%3gen-def%1]⊗↓%dI%1[%3gen-def%1] is of the form %3$gendef $fundef↑*
%1in the intermediate language.← =\%3"(" "generic" gname id-list\gen-def =
\ %dSelect%1[[%3choice "choices?"%1]%3↑*%1] ")"\%3"generic" gname
\ %dMake-defs%1[%3id-list, \"parameter list?" id-list
\ %1[%3choice "choices?"%1]%3↑*\%3"choices?" %1[%3choice "choices?"%1]%3↑* "."
\ bodydef↑*%1]\%3"body-defs:" body-def↑*
.fp
%1where:
%dSelect%1[%7e%1] =\%7e%1\where %7e%1 is the empty string
%dSelect%1[%3choice%41%3 "choices?" %1[%3choice "choices?"%1]%3↑*%1] =
\%dSelect%1[%3choice%41%1] %dSelect%1[[%3choice "choices?"%1]%3↑*%1]
%dSelect%1[%3choice%1] =\%3input-pattern fname\choice =
\\ input-pattern
\\ "function name?" fname
\\ "precond?" precondition
\\ "postcond?" postcondition
\\ "body name?" bname
%dMake-defs%1[%3id-list,%1[%3choice "choices?"%1]%3↑*, %7e%1] = %7e%3
%dMake-defs%1[%3id-list,%7e%3, body-def↑*%1] = %7e%3
%dMake-defs%1[%3id-list, choice%41%3 "choices?" %1[%3choice "choices?"%1]%3↑*, body-def↑*%1] =
\%dMake-def%1[%3id-list, choice%41%3, %dBody-of%1[%3choice%41%1, %3body-def↑*%1]]
\%dMake-defs%1[%3id-list, %1[%3choice "choices?"%1]%3↑*, body-def↑*%1]
\%dBody-of%1[%3choice, body-def↑*] =\the %3body-def%1 whose %3bname%1
\\is mentioned in %3choice%1.
%dMake-def%1[%3id-list, choice, body-def%1] =
\%3"(" "function" fname \choice =
\input-pattern id-list precondition\ input-pattern
\postcondition %dI%1[%3h-clause↑*%1]%3 ")"\ "function name?" fname
\\ "precond?" precondition
\\ "postcond?" postcondition
\\ "body name?" bname
\\body-def =
\\ bname h-clause↑* "."
.fp
%1Finally,
%dI%1[%3target-def%1] =\%3"(" "setq" "target"\%3target-def =
\ target-language ")"\"target" target-language
.end "spec5"
The target language specification is just information to the system
indicating which target language is desired and is of interest only in choosing
the mapping
from intermediate language to target.
The specification of the factorial function:
.begin nofill;select 3
.group
%3function Fact
input pattern? (1 0)
parameter list? (x y)
precond? Integer(x, true) ∧ ≥(x, 0, true).
postcond? Integer(y, true) ∧ >(y, 0, true).
body? Fact(0, 1)
Fact(z, w) ← Sub1(z, z1), Fact(z1, w1), *(z, w1, w).
.apart
.end
has the following form in the Intermediate Language:
.begin nofill;select 3
.group
%3(function Fact (1 0) (!x !y)
(∧ (Integer !x true) (≥ !x 0 true))
(∧ (Integer !y true) (> !y 0 true))
(bktrkcond ((0 1) (try))
((!z !w) (try (Sub1 !z !z1)
(Fact !z1 !w1)
(* !z !w1 !w) ) )
) )
.apart
.end
.sec(Correctness of the Mapping to Intermediate Form)
We wish to show that the semantics of an input specification is "sufficiently"
preserved in the mapping to intermediate form. By "sufficiently" we mean that
the semantics of the intermediate form of a function definition is implied by the
semantics of the input specification, and furthermore, if every function
(or type) %3P%1 is defined such that for each input tuple, %g¬%3x%4i%1,
(i.e., tuple with which the function is called) there exists a unique
output tuple, %g¬%3x%4o%1,
such that %3P(%g¬%3x%4o%3)%1 is derivable using the input semantics,
then %3P(%g¬%3x%4o%3)%1 is derivable using the semantics of the intermediate
form of the definition. We refer to this restriction of requiring uniqueness
of the output tuple by saying that we are defining only "functional" relationships.
The semantics of input and internal form are not equivalent because the input
semantics may be used several ways to generate proofs. This is due to the
nondeterministic nature of the process of finding proofs. At any stage of a
proof, there may
be many Horn clauses that are applicable as axioms, and different proof paths
may generate different results. However, we have restricted ourselves
to defining functional relationships rather than the more general "relations"
which may be one-to-many mappings. Thus, no matter what direction the proof
takes, there is a unique result. If a function is specified that does not
return unique answers, then the resulting program (and any others whose specifications
make use of the function) will be partially correct;
however we cannot guarantee that any specification using such a function
will result in a program that always finds an answer when one exists.
In the intermediate form we are forced to
apply the Horn-clauses in a specific order.
Due to the determinism introduced we will follow precisely one proof, the same proof,
every time a procedure gets called with the same input values. The important
point to establish is that whenever a unique answer may be found in the
nondeterministic proof process, our deterministic search will find it as well.
First, we establish two lemmas.
.fp
%2Lemma 1.1
.begin center;turn on "↑"
∀%g¬%2x S[%3h-clause↑*%2] → S[%dI%2[%3h-clause↑*%2]]
.end
.begin nofill;turn on "↑[]&↓"
%1that is
%2∀%g¬%2x [
%9∧%6↑n&↓i↓=↓1%2 (name arglist%4i%2 ← %2S[%3subgoals%4i%2]) →
%9∧%6↑n&↓i↓=↓1%2
(unify[id-list, arglist%4i%2] = %7s%4i%2) ∧ %9∧%6↑[i -1]&↓[j =1]%2 ¬(%2S[%dI%2[%3subgoals%4j%2]%7s%4j%2]) →
(%2S[%dI%2[%3subgoals%4i%2]%7s%4i%2] → %2S[%dI%2[%3name arglist%4i%2]%7s%4i%2]) ]
.end
%1where %2∀%g¬%2x%1 stands for the universal quantification of all variables
mentioned in the quantified formula.
.fp
Proof:
.begin indent 15,10,10
We shall show that for each i, %2S[%3h-clause%2] → S[%dI%2[%3h-clause%2]]. %1For the
sake of readability we shall leave out the quantifier with the understanding that
all variables are universally quantified.
Thus, we want to show:
.begin nofill; turn on "↑[]&↓";tabit1(50)
%2(name arglist%4i%2 ← %2S[%3subgoals%4i%2]) →
( (unify[id-list, arglist%4i%2] = %7s%4i%2) ∧
%9∧%6↑i&↓ ↑ &↓j↑-&↓=↑1&↓1%2 ¬(%2S[%dI%2[%3subgoals%4j%2]%7s%4j%2]) →
(%2S[%dI%2[%3subgoals%4i%2]%7s%4i%2] → S[%dI%2[%3name arglist%4i%2]%7s%4i%2]) )
1. %2S[%3subgoals%4i%2] → name arglist%4i%1 \hypothesis
%22. [%2S[%3subgoals%4i%2] → name arglist%4i%2]%7s%4i%1 \%2∀%1x A(x) %br%1 A(t)
\(as many times as necessary, given
\that we change variable names that
\are introduced by the substitution
\in order to ensure that the new
\variables are %3free for%1⊗↓For a formal definition of %3free for%1 see Davis [D 76],
Kleene [K 52], or Mendelson [M 64].← the old.
%23. [%2S[%dI%2[%3subgoals%4i%2]] → S[%dI%2[%3name arglist%4i%2]]]%7s%4i%1\from %22.%1, equivalent replacement,
\and the facts that
\%2S[%dI%2[%3subgoals%4i%2]] ≡ %2S[%3subgoals%4i%2]%1
\and %2S[%dI%2[%3name arglist%4i%2]] ≡ %2S[%3name arglist%4i%2]
4. %2S[%dI%2[%3subgoals%4i%2]%7s%4i%2] → S[%dI%2[%3name arglist%4i%2]]%7s%4i%2\%1property of substitution
%25. (unify[id-list, arglist%4i%2] = %7s%4i%2) \%1A → (B → A) and %24.%1, and Modus Ponens
∧ %9∧%6↑[i -1]&↓[j =1]%2 ¬%2S[%dI%2[%3subgoals%4j%2]%7s%4j%2]
→ (%2S[%dI%2[%3subgoals%4i%2]%7s%4i%2] → S[%dI%2[%3name arglist%4i%2]]%7s%4i%2)
6. %2(name arglist%4i%2 ← %2S[%3subgoals%4i%2]) →\%1Deduction Theorem, %21.,5.
( (unify[id-list, arglist%4i%2] = %7s%4i%2) ∧
%9∧%6↑i&↓ ↑ &↓j↑-&↓=↑1&↓1%2 ¬%2S[%dI%2[%3subgoals%4j%2]%7s%4j%2] →
(%2S[%dI%2[%3subgoals%4i%2]%7s%4i%2] → S[%dI%2[%3name arglist%4i%2]%7s%4i%2]) )%1
QED
.end
.end
.begin nofill; tabit1(45)
The following lemma makes use of two sub-lemmas whose proofs follow it.
.fp
%2Lemma 1.2
.begin center
%2∀%g¬%2x (Y → Y%9'%2) %br%2 ∀%g¬%2x(X → Y ∧ Z) → ∀%g¬%2x(X → Y%9'%2 ∧ Z)
.end
.begin fill;single space
where %2X%1, %2Y%1, %2Y%9'%1,and %2Z%1 are any well-formed-formulas. The
proof is given for a single
quantified variable. Clearly it can be generalized to any number of variables.
.end
%21. ∀x(X → Y ∧ Z)\%1hypothesis
%22. ∀x(X → Y)\%21., Lemma 1.2.1
%23. X → Y \2., %1∀-elimination
%24. ∀x(Y → Y%9'%2)\%1hypothesis
%25. Y → Y%9'%2\4., %1∀-elimination
%26. X → Y%9'%2\3.,5.,%1 transitivity of →
%27. ∀x(X → Y%9'%2)\6.,%1 ∀-introduction
%28. ∀x(X → Z)\1., Lemma 1.2.1
9. ∀x(X → Y%9'%2 ∧ Z)\7.,8., Lemma 1.2.2
9. ∀x(X → Y ∧ Z) → ∀x(X → Y%9'%2 ∧ Z)\ 1.,9., %1Deduction Theorem
.end
.begin indent 15,15,15; tabit1(45)
%2Lemma 1.2.1
.begin center
∀x(X → Y ∧ Z) %br%2 ∀x(X → Y)
%1we will derive the above version, and by commutativity of ∧ assume that we also have
%2∀x(X → Y ∧ Z) %br%2 ∀x(X → Z)
.end
1. ∀x(X → Y ∧ Z)\%1hypothesis
%22. X → Y ∧ Z\%2∀%1-elimination
%23. X\%1hypothesis
%24. Y ∧ Z\2.,3.,%1 Modus Ponens
%25. Y\%1∧-elimination
%26. X → Y\3.,5., %1Deduction Theorem
%27. ∀x(X → Y)\6., %2∀%1-introduction
%2Lemma 1.2.2
.begin center
∀x(X → Y), ∀x(X → Z) %br%2 ∀x(X → Y ∧ Z)
.end
1. ∀x(X → Y)\%1hypothesis
%22. X → Y\1., %2∀%1-elimination
%23. ∀x(X → Z)\%1hypothesis
%24. X → Z\3., %2∀%1-elimination
%25. X\%1hypothesis
%26. Y\2.,5., %1Modus Ponens
%27. Z\4.,5., %1Modus Ponens
%28. Y ∧ Z\%1∧-introduction
%29. X → Y ∧ Z\5.,8., %1Deduction Theorem
%210. ∀x(X → Y ∧ Z)\%2∀%1-introduction
.end
We are now in a position to prove our first theorem.
.begin nofill
%2Theorem 1 :
.end
.begin center
%2S[%dI%2[%3input%2]] %br%2 P(%g¬%2x)%2 => S[%3input%2] %br%2 P(%g¬%2x)%1
.end
Any proof derived from the semantics of the intermediate form could be derived
from the semantics of the input specification. We will show this by determining
that the semantics
of an input specification implies the semantics of the intermediate
form of the specification.
.fp
Proof:
.begin indent 6,6,6
Since %3input%1 is a sequence of definitions which gets internalized as a sequence
of definitions, we shall show that:
.begin center
%2S[%3definition%2] → S[%dI%2[%3definition%2]]%1
.end
.pt24
.indent 6,6,6
Then the conjunction of the input definitions implies the conjunction of the
intermediate language form of those definitions and:
.begin center
%2S[%3input%2] → S[%dI%2[%3input%2]]%1
.end
.pt24
.indent 6,6,6
and thus anything derivable from %2S[%dI%2[%3input%2]]%1 can be derived from
%2S[%3input%2]%1 by first deriving %2S[%dI%2[%3input%2]]%1 and then following the same
proof. We must establish two things:⊗↓Recall that %dI%1 is just the identity mapping
on %3id-list%1's, %3input-pattern%1's, and %3name%1's.←
.end
.begin nofill;turn on "↑&↓"
1) for function and type definitions⊗↓The semantics of a type definition is the
same as that for a function definition. We gave them separately before, pointing
out that we know what the id-list, input-pattern, precondition, and
postcondition are for type definitions.←:
%2[ ∀%g¬%2x defined[ inputs[S[%3id-list%2], S[%3input-pattern%2]] ] ∧ S[%3precondition%2]
→ S[%3h-clause↑*%2] ∧ ( (S[%3name%2] S[%3id-list%2]) → S[%3postcondition%2]) ]
→
%2[ ∀%g¬%2x defined[ inputs[S[%3id-list%2], S[%3input-pattern%2]] ] ∧ S[%dI%2[%3precondition%2]
→ S[%dI%2[%3h-clause↑*%2]] ∧ ( (S[%3name%2] S[%3id-list%2]) → S[%dI%2[%3postcondition%2]) ]
%12) for generic definitions:
%9∧%6↑n&↓i↓=↓1%2 ∀%g¬%2x [
(S[%3funname%4i%3 id-list%2] → S[%3name id-list%2]) ∧
( defined[ inputs[S[%3id-list%2], S[%3input-pattern%4i%2]] ] ∧ S[%3precondition%4i%2]
→ S[H-C[%3body-name%4i%2]] ∧ (S[%3funname%4i%3 id-list%2] → S[%3postcondition%4i%2]) ) ]
→
%9∧%6↑n&↓i↓=↓1%2 ∀%g¬%2x [
(S[%3funname%4i%3 id-list%2] → S[%3name id-list%2]) ∧
( defined[ inputs[S[%3id-list%2], S[%3input-pattern%4i%2] ] ∧ S[%dI%2[%3precondition%4i%2]]
→ S[%dI%2[H-C[%3body-name%4i%2]]] ∧ (S[%3funname%4i%3 id-list%2] → S[%dI%2[%3postcondition%4i%2]]) ) ]
%1where %2H-C[%3body-name%4i%2]%1 is the %3h-clause↑*%1 associated with %3body-name%4i%1.
.end
.begin indent 10,6,6
%11) is of the form %2∀%g¬%2x (A ∧ B → C ∧ D) → ∀%g¬%2x (A ∧ B → C%9'%2 ∧ D)%1, where we
know by %2Lemma 1.1%1 that %2∀%g¬%2x(C → C%9'%2)%1.
Thus, this is just an instance of %2Lemma 1.2 with
"%2A ∧ B%1" for %2X%1, "%2C%1" for %2Y%1, "%2C%9'%1" for %2Y%9'%1, and "%2D%1" for %2Z%1.
.indent 10,6,6
2) for each i, is of the form %2∀%g¬%2x[(A → B) ∧ (C ∧ D → E ∧ F)] →
∀%g¬%2x[(A → B) ∧ (C ∧ D → E%9'%2 ∧ F)]%1.
This is just %2X ∧ Y → X ∧ Y%9'%1, where we know by part 1) that %2Y → Y%9'%1. For each i,
the statement is true, thus the conjunction of statements over all i's is true.
.end
.begin indent 70,0,0
QED
.end
.fp
%2Theorem 2:
%1If each definition is functional with respect to its output variables,
that is, if for each function or type %2P%1 and each input tuple %g¬%2x%4i%1,
there exists a unique output tuple, %g¬%2x%4o%1, such that %2P(%g¬%2x%4o%2)%1, then:
.begin center
%2S[%3input%2] %br%2 P(%g¬%2x%4o%2) %2=> S[%dI%2[%3input%2]] %br%2 P(%g¬%2x%4o%2)%1
.end
.fp
Proof:
.begin indent 10,6,6
Given a proof of %2P(%g¬%2x)%1 from %2S[%3input%2]%1 we can construct a proof from
S[%dI%2[%3input%2]]%1. A clause of the definition of %2P%1 is applicable if and
only if the current goal is an instance of the head of the clause, i.e.,
there is a %7s%4i%1
such that %2unify[id-list, arglist%4i%2] = %7s%4i%1 where %2id-list%1 is bound to
the actual parameters in the goal. Thus the only time when a clause that is
applicable in the proof from %2S[%3input%2]%1 may not be used in a proof from
S[%dI%2[%3input%2]]%1 is when there is a previously listed clause that is also
applicable.
.indent 10,6,6
Suppose the proof of %2P(%g¬%2x)%1 makes use of the clause %2P%4i%1 of the definition
of %2P%1 when there is a clause %2P%4j%1, j<i, that is also applicable. Our proof
from S[%dI%2[%3input%2]]%1 will attempt to prove %2P(%g¬%2x)%1 using %2P%4j%1.
We are guaranteed termination of this attempt by the
precondition. If we terminate successfully, we will have proved
%2P(%g¬%2x)%1, since this proof may also be considered a proof from %2S[%3input%2]%1
and we have assumed that %g¬%2x%1 is unique. If we terminate unsuccessfully,
then we will attempt another clause, possibly %2P%4i%1 now, as in the original
proof from %2S[%3input%2]%1, or possibly some %2P%4k%1, j<k<i. We will eventually
succeed before attempting %2P%4i%1, or we will use %2P%4i%1 as we did in
the original proof. The same analysis is applicable to every clause used in the
proof of %2P(%g¬%2x)%1 from %2S[%3input%2]%1 and thus we can derive %2P(%g¬%2x)%1
from S[%dI%2[%3input%2]]%1.
.indent 70,0,0
QED
.end
.sec(Mapping the Intermediate Language to LISP)
We have chosen to use LISP as the first target language. One may find
documentation for the version we use, MACLISP, in [M 74]. We generate
"pure LISP" programs, using none of the special features of the MACLISP
implementation, however the names of the primitive functions may vary
from implementation to implementation. These functions include: %3defun%1,
for defining a function, %3putprop%1, for putting a property on the
property list of an atom, and %3get%1, for getting a property from the
property list.
The function %dL%1, mapping the intermediate language into LISP is defined
as follows.
.begin nofill;turn on "↑";tabit2(30,60)
%dL%2[%7e%2] =\%7e%1
%dL%2[%3$definition%41%3 $definition↑*%2] =\%dL%2[%3$definition%41%2] %dL%2[%3$definition↑*%2]
%dL%2[%3$definition%2] =\%dL%2[%3$fun-def%2]\%3$definition = $fun-def
%dL%2[%3$definition%2] =\%dL%2[%3$type-def%2]\%3$definition = $type-def
.tabit2(18,60)
%dL%2[%3$fun-def%2] =\%3"(putprop" "'"$name \$fun-def =
\ "'"$input-pattern "'inpat)"\"(" "function" $name
\"(putprop" "'"$name "'"$id-list \ $input-pattern
\ "'params)"\$id-list $precondition
\"(putprop" "'"$name "'"$precondition \$postcondition "("
\ "'precond)"\"bktrkcond" $alternatives ")" ")"
\"(putprop" "'"$name "'"$postcondition
\ "'postcond )"
\"(defun" $name "fexpr (l)"
\ "(bktrkcond l" "'"$alternatives"))"
%dL%2[%3type-def%2] =\%3"(putprop" "'"$name \type-def =
\ "'(1 0) 'inpat)"\ "(" "type" $name
\"(putprop "'"$name "'(x y)"\ "(1 0)" "(x y)"
\ "'params)"\ "T" "(boolean y)"
\"(putprop "'"$name \ "(" "bktrkcond"
\ "'T 'precond)"\ $alternatives ")" ")"
\"(putprop "'"$name
\ "'(boolean y) 'postcond)"
\"(defun" $name "fexpr (l)"
\ "(bktrkcond l "'"$alternatives"))"%1
.end
There is no mapping of generic definitions, only of the specific function definitions
involved, and these are identical to that for %3fun-def'%1s above.
The LISP function %3bktrkcond%1 evaluates its arguments, binds the results
to the formal parameters %3actuals%1 and %3list-alts%1, and then
recursively attempts each
alternative until an answer is found or all alternatives have failed, indicating
that the answer is undefined. The complete set of definitions of LISP functions
that implement the mapping, i.e. definitions for %3bktrkcond, match, try%1, and
all of the subfunctions required, may be found in {yonss (P13)}, beginning at
{yon (P8)}.
The LISP program that is generated from the specification for the factorial
function is as follows. The list of %3putprop%1's get evaluated only once;
they represent global information about the properties of the function. The
%3defun%1 is the actual LISP definition of the function.
.begin nofill;select 3
.group
(defun Fact fexpr (l)
(cond ((true-precond (cons 'Fact l))
(bktrkcond l
'(((0 1) (try))
((!x !y)
(try (Sub1 !x !x1)
(Fact !x1 !y1)
(* !x !y1 !y))))))
(t 'undef)))
.apart
.end
.sec(Correctness of the Mapping to LISP Program)
We shall show that the semantics of the LISP form of a function or type definition
is equivalent to the semantics of the intermediate form of a function or type
definition. There is no distinction between function and type definitions
in either form.
We have shown earlier that the semantics of the intermediate form of a definition
is expressed:
.begin nofill; turn on "↑[]&↓"
%2∀%g¬%2x defined[ inputs[$id-list, $input-pattern] ] ∧ $precondition →
%9∧%6↑n&↓i↓=↓1%2 [
(unify[$id-list, $arglist%4i%2] = %7s%4i%2)
∧ %9∧%6↑[i-1]&↓[#j=1]%2#(unify[$id-list, $arglist%4j%2] = %7s%4j%2 → ¬%2S[%3$subgoals%4j%2%7s%4j%2])
→ ( %2S[%3$subgoals%4i%2%7s%4i%2] → ($name $arglist%4i%2)%7s%4i%2 ) ]
∧
∀%g¬%2x $name $id-list → $postcondition%1
.end
Since %2$arglist%4i%1 and %2$id-list%1 are unified by %7s%4i%1, we can use %2$name $id-list%1
instead of %2$name $arglist%4i%1 in the final consequent of the first conjunct above.
Another way of expressing the fact that %2$name $id-list%1 is true is by saying that
%2$id-list ε $name%1, that is, the given tuple is an element of the relation %2$name%1.
Before turning our attention to the semantics of the LISP form, we shall rewrite the
semantics of the intermediate form in such a way as to facilitate our proof. This
rewriting is based on several rules of first-order logic. To make the
statements more readable, we shall look at the general form of the rewrite first,
and then apply the result to the expression above.
We are going to focus our attention on the first conjunct of the above expression.
This is of the form:
.begin center
%2∀%g¬%2x A → %9∧%6↑n&↓i↓=↓1%2 [B ∧ C → (D → E)]
%1which is equivalent to
%2∀%g¬%2x A → ∀i [B ∧ C → (D → E)]
.end
.fp
%1where actually the quantifier on %2i%1 is bounded. Since we know there are a finite number
of i's we will not put in the bounds. It should be understood that i ranges over
the number of clauses given in the definition.⊗↓The "variable" %2i%1 is not really
a variable at all in the formal sense; it is merely an index. We could write out the
consequence of the above implication as the conjunction of the indexed statements.
We are using the "%2∀i%1" notation because it provides a convenient abbreviation.←
The above statement is in turn equivalent to
.begin center
%2∀%g¬%2x A → ∀i [(B ∧ C ∧ D) → E]
.end
%1Since in our original formula %2E%1 does not contain any free occurrences of i,
this is equivalent to:
.begin center
%2∀%g¬%2x A → [∃i(B ∧ C ∧ D) → E]
.end
Thus our new formulation of the semantics of the intermediate form of a function
(or type) definition is:
.begin nofill; turn on "↑[]&↓"
%2∀%g¬%2x defined[ inputs[$id-list, $input-pattern] ] ∧ $precondition →
[ ∃i ( unify[$id-list, $arglist%4i%2] = %7s%4i%2
∧ %9∧%6↑[i-1]&↓[#j=1]%2#(unify[$id-list, $arglist%4j%2] = %7s%4j%2 → ¬%2S[%3$subgoals%4j%2%7s%4j%2])
∧ %2S[%3$subgoals%4i%2%7s%4i%2] )
→ ($id-list)%7s%4i%2 ε $name) ]
∧
∀%g¬%2x ($id-list ε $name) → $postcondition%1
.end
The semantics of a LISP form of a definition, such as:
.begin nofill;select 3
(putprop $name $input-pattern 'inpat)
(putprop $name $id-list 'params)
(putprop $name $precondition 'precond)
(putprop $name $postcondition 'postcond)
(defun $name fexpr (l)
(cond ((true-precond (cons $name l))
(bktrkcond l (rest $body-def)))
(t undef)))
.fp
%1is:
%2∀%g¬%2x [ eval[(cons $name actuals)] = %7s%2 ∧ %7s%2 ≠ undef → (actuals)%7s%2 ε $name ]
∧ ∀%g¬%2x[ (actuals ε $name) → $postcondition]
%1where: %7s%2 is a substitution or %7s%1 = %2undef%1
%2actuals%1 is an instantiation of %3$id-list
%3$body-def%1 is %3(bktrkcond ($arglist%41%3 (cons 'try $subgoals%41%3))
($arglist%42%3 (cons 'try $subgoals%42%3))
...
($arglist%4n%3 (cons 'try $subgoals%4n%3)))
.end
%1The actual function definition begins with %3defun%1, the preceeding %3putprop%1's
simply attach the listed information to the property list of the function being
defined. See [MT 79] for a formal axiomatization of the semantics of LISP.
%1Using the definitions of %2eval%1 and %2$name%1, we can write:
.begin nofill
%2eval[(cons $name actuals)] =
IF true-precond[(cons $name actuals)]
THEN bktrkcond[actuals, rest[$body-def]]
ELSE undef
%1thus,
.begin center
%2eval[(cons $name actuals)] = %7s%2 ∧ %7s%2≠ undef
%1 is equivalent to
%2true-precond[(cons $name actuals)] ∧ bktrkcond[actuals, rest[$body-def]] = %7s%2
∧ %7s%2 ≠ undef
.end
%1So we can rewrite the semantics of the LISP form as:
%2∀%g¬%2x [ true-precond[(cons $name actuals)]
∧ bktrkcond[actuals, (($arglist%41%2 (cons 'try $subgoals%41%2))
($arglist%42%2 (cons 'try $subgoals%42%2))
...
($arglist%4n%2 (cons 'try $subgoals%4n%2)))] = %7s%2
∧ %7s%2 ≠ undef
→ (actuals)%7s%2 ε $name ]
∧ %2∀%g¬%2x [(actuals ε $name) → $postcondition]
.end
%1 We need to establish that the above statement is equivalent to the statement of
the semantics of the intermediate form of definition given above. We intend
to show this by first establishing that:
.begin nofill;turn on "↑[]&↓"
%2∀%g¬%2x [
[defined[inputs[$id-list, $input-pattern]] ∧ $precondition] →
[ ∃i ( unify[$id-list, $arglist%4i%2] = %7s%4i%2
∧ %9∧%6↑[i-1]&↓[#j=1]%2#(unify[$id-list, $arglist%4j%2] = %7s%4j%2 → ¬%2S[%3$subgoals%4j%2%7s%4j%2])
∧ %2S[%3$subgoals%4i%2%7s%4i%2] )
→ ($id-list)%7s%4i%2 ε $name) ]
≡
[ true-precond[(cons $name actuals)]
∧ bktrkcond[actuals, (($arglist%41%2 (cons 'try $subgoals%41%2))
($arglist%42%2 (cons 'try $subgoals%42%2))
...
($arglist%4n%2 (cons 'try $subgoals%4n%2)))] = %7s%2
∧ %7s%2 ≠ undef
→ (actuals)%7s%2 ε $name ] ]
.end
%1The expression resulting from distributing the %2∀%g¬%2x%1 over the equivalence
follows easily from this stronger result. First of all,
we will simplify the notation. Both %2$id-list%1 in the intermediate form and %2actuals%1
in the Lisp form are names used to refer to instantiations of the formal parameter
list. Since these are now within the scope of the same universal quantifier, we
shall identify them both by the same name, %2actuals%1. We should also mention that
%2precondition%1 and %2postcondition%1 are names that are being used to stand
for the formulas they represent. Each involves some of the elements of the formal
parameter list and we shall assume that there is no confusion as to the bindings
of these variables even though we do not mention them explicitly in the formula.
Before attempting the main theorem of this section, we need four lemmas:
.begin nofill;turn on "↑[]&↓"
%21. defined[inputs[actuals, $input-pattern]] ∧ $precondition
≡ true-precond[(cons $name actuals)]
2. unify[actuals, $arglist%4i%2] = %7s%4i%2
≡ match[actuals, newversion[$arglist%4i%2]] = %7s%4i%2 ∧ %7s%4i%2 ≠ undef
3. %2S[%3$subgoals%2] ≡ try[$subgoals] = %7s%2 ∧ %7s%2 ≠ undef
4. ∃i ( unify[$id-list, $arglist%4i%2] = %7s%4i%2
∧ %9∧%6↑[i-1]&↓[#j=1]%2#(unify[$id-list, $arglist%4j%2] = %7s%4j%2 → ¬%2S[%3$subgoals%4j%2%7s%4j%2])
∧ %2S[%3$subgoals%4i%2%7s%4i%2] )
≡
bktrkcond[actuals, (($arglist%41%2 (cons 'try $subgoals%41%2))
($arglist%42%2 (cons 'try $subgoals%42%2))
...
($arglist%4n%2 (cons 'try $subgoals%4n%2)))] = %7s%2
∧ %7s%2 ≠ undef
.end
%1 We intend to show that the top level mapping is correct, however
we do not intend to prove the entire implementation correct, so the proofs
of these lemmas will be informal and assume correctness of several subfunctions
involved.
%2Lemma 1
.begin center
defined[inputs[actuals, $input-pattern]] ∧ $precondition
≡ true-precond[(cons $name actuals)]
.end
.fp
%1Proof:
.begin indent 10,6,6
The function %2true-precond%1: 1) looks up the %2$input-pattern%1 associated with
%2$name%1 and checks to see that all input positions of %2actuals%1 have values supplied;
then 2)looks up the %2$id-list%1 and %2$precondition%1 associated with %2$name%1,
binds the variables in %2$id-list%1 to the values supplied by %2actuals%1 and
evaluates the %2$precondition%1. Thus, %2true-precond%1 returns "true" if and only
if both steps1) and 2) are successful, i.e., if and only if %2defined[inputs[actuals,
$input-pattern]] ∧ $precondition.%1
.indent 70,0,0
QED
.end
.group
%2Lemma 2
.begin center
unify[actuals, $arglist%4i%2] = %7s%4i%2
≡ match[actuals, newversion[$arglist%4i%2]] = %7s%4i%2 ∧ %7s%4i%2 ≠ undef
.end
.apart
.fp
%1Proof:
.begin indent 10,6,6
The semantic function %2unify%1, attempts to unify its arguments after renaming
variables so its arguments have no variable in common. If unification is
possible, then %2unify%1 returns a substitution, if not, then %2unify[actuals, $arglist%4i%2]
≠ %7s%1 for any substitution %7s%1, so the result is false.
.indent 10,6,6
%2newversion[$arglist]%1 generates a new version of %2$arglist%1 in which each variable
has been replaced by a newly generated one. Thus, %2newversion%1 ensures that the
arguments to %2match%1 have been standardized apart. %2match%1 is a unification
algorithm that returns a (most general) substitution %7s%1 if its arguments are
unifiable by %7s%1, and returns %2undef%1 if unification is not possible. Thus,
.begin center
%2unify[actuals, $arglist%4i%2] = %7s%4i%2
≡
match[actuals, newversion[$arglist%4i%2]] = %7s%4i%2 ∧ %7s%4i%2 ≠ undef
.end
.indent 70,0,0
QED
.end
%2Lemma 3
.begin center
%2S[%3$subgoals%2] ≡ try[$subgoals] = %7s%2 ∧ %7s%2 ≠ undef
.end
.fp
%1Proof:
.begin indent 10,6,6
Each subgoal is a function application %2P(x1,...,xn)%1 that is true if and only
if the %2precondition%1 on the input arguments is true and there exists a
substitution %7s%1 such that %2(x1,...xn)%7s%1 is the unique output tuple
associated with %2(x1,...,xn)%1 by %2P%1. For the conjunction of a list of
subgoals to be true, each must be true, and, since all their variables are
bound by the same universal quantifier, a value supplied to a variable in the
evaluation of one subgoal is propagated to all occurrences of that variable
throughout the list of subgoals. Thus, %2S[%3$subgoals%2]%1 is true if and only if
there exists a substitution %7s%1 such that %2subgoal%41%7s%2 ∧ subgoal%42%7s%2 ∧ ...
∧ subgoal%4n%7s%1.
.indent 10,6,6
All of this is implicit in the semantics of the intermediate form, simply a
property of bound variables. The LISP form makes it all explicit by requiring
that evaluation of %2P(x1,...,xn) = %7s%1 where %7s%1 is the substitution such
that %2(x1,...,xn)%7s%1 is the unique tuple associated with %2(x1,...,xn)%1 by
%2P%1. If there does not exist any such substitution then %2try%1 returns %2undef%1.
.end
.begin nofill
%2try[($subgoal%41%2, ..., $subgoal%4n%2)] =
IF eval[$subgoal%41%2] = %7s%2 ∧ %7s%2 ≠ undef
∧ try[mk-subst[($subgoal%42%2, ..., $subgoal%4n%2), %7s%2]] = %7s%9'%2
∧ %7s%9'%2 ≠ undef
THEN %7s%fo%7s%9'%2
ELSE undef
.end
.begin indent 10,6,6
%1Note that since substitutions are made as you go, and evaluations that cause binding
to variables always create new variables to bind to, we know that ∀x such that
%7s%1 contains a binding, say x/a, there does not exist in %7s%1 any binding of the
form x/y where y≠a, or any binding of the form y/z where z contains x. Thus,
.begin center
%2S[%3$subgoals%2] ≡ try[$subgoals] = %7s%2 ∧ %7s%2 ≠ undef%1.
.end
.indent 70,0,0
QED
.end
%2Sublemma 4.1
.fp
%1A recursive definition of the form:
.begin nofill;turn on "↑[]&↓"
%2 f[u] = IF null[u] THEN undef
ELSE IF P[first[u]] THEN g[first[u]]
ELSE f[rest[u]]
%1has the property that, if %2u = (u%41%2 u%42%2 ... u%4n%2)%1, then
%2 f[u] = a ∧ a ≠ undef ≡
∃i( g[u%4i%2] = a ∧ a ≠ undef ∧ P[u%4i%2] ∧ (%9∧%6↑[i-1]&↓[#j=1]%2# ¬P[u%4j%2]) )
.end
%1This is a direct consequence of the definition of %2f%1, which specifies that each
element of %2u%1 is tested in the order given, and that no element is tested unless
all before it in the list have been tried and have failed. We prove it by induction
on the length of the list %2u%1.
.begin nofill
Basis: %2u = (u%41%2)
f[(u%41%2)] = IF null[(u%41%2)] THEN undef
ELSE IF P[u%41%2] THEN g[u%41%2]
ELSE f[()]
= IF false THEN undef
ELSE IF P[u%41%2] THEN g[u%41%2]
ELSE IF null[()] THEN undef
ELSE ...
= IF P[u%41%2] THEN g[u%41%1]
ELSE undef
%1Thus, %2f[(u%41%2)] = a ∧ a ≠ undef ≡ P[u%41%2] ∧ g[u%41%2] = a ∧ a ≠ undef
%1Induction Step: Assume that for all lists of length ≤ n:
%2 f[u] = a ∧ a ≠ undef ≡
∃i( g[u%4i%2] = a ∧ a ≠ undef ∧ P[u%4i%2] ∧ (%9∧%6↑[i-1]&↓[#j=1]%2# ¬P[u%4j%2]) )
f[(u%41%2 ... u%4(n+1)%2)] =
IF null[(u%41%2 ...u%4(n+1)%2)] THEN undef
ELSE IF P[u%41%2] THEN g[u%41%2]
ELSE f[(u%42%2 ... u%4(n+1)%2)]
=
IF false THEN undef
ELSE IF P[u%41%2] THEN g[u%41%2]
ELSE f[(u%42%2 ... u%4(n+1)%2)]
=
IF P[u%41%2] THEN g[u%41%2]
ELSE f[(u%42%2 ... u%4(n+1)%2)]
%1thus, %2f[(u%41%2 ... u%4(n+1)%2)] = a ∧ a ≠ undef
≡
(P[u%41%2] ∧ g[u%41%2] = a ∧ a ≠ undef)
∨ (¬P[u%41%2] ∧ f[(u%42%2 ... u%4(n+1)%2)] = a ∧ a ≠ undef)
≡
(i=1 ∧ g[u%4i%2] = a ∧ a ≠ undef ∧ P[u%4i%2] ∧ (%9∧%6↑[i-1]&↓[#j=1]%2# ¬P[u%4j%2]) )
∨ (¬P[u%41%2] ∧ ∃i( g[u%4i%2] = a ∧ a ≠ undef ∧ P[u%4i%2] ∧ (%9∧%6↑[i-1]&↓[#j=2]%2# ¬P[u%4j%2])))
≡
∃i( g[u%4i%2] = a ∧ a ≠ undef ∧ P[u%4i%2] ∧ (%9∧%6↑[i-1]&↓[#j=1]%2# ¬P[u%4j%2])))
.indent 70,0,0
QED
.end
%2Lemma 4
.begin nofill;turn on "↑[]&↓"
∃i ( unify[$id-list, $arglist%4i%2] = %7s%4i%2
∧ %9∧%6↑[i-1]&↓[#j=1]%2#(unify[$id-list, $arglist%4j%2] = %7s%4j%2 → ¬%2S[%3$subgoals%4j%2%7s%4j%2])
∧ %2S[%3$subgoals%4i%2%7s%4i%2] )
≡
bktrkcond[actuals, (($arglist%41%2 (cons 'try $subgoals%41%2))
($arglist%42%2 (cons 'try $subgoals%42%2))
...
($arglist%4n%2 (cons 'try $subgoals%4n%2)))] = %7s%2
∧ %7s%2 ≠ undef
.fp
%1proof:
Let %2$alternatives = (($arglist%41%2 (cons 'try $subgoals%41%2))
($arglist%42%2 (cons 'try $subgoals%42%2))
...
($arglist%4n%2 (cons 'try $subgoals%4n%2)))
%1then, %2bktrkcond[actuals, $alternatives] =
IF null[$alternatives] THEN undef
ELSE IF match[actuals, newversion[$arglist%41%2]] = %7s%41%2 ∧ %7s%41%2 ≠ undef
∧ try[$subgoalist%41%2%7s%41%2] = %7s%41%9'%2 ∧ %7s%41%9'%2 ≠ undef
THEN cleanup[%7s%41%fo%7s%41%9'%2, actuals]
ELSE bktrkcond[actuals, (($arglist%42%2 cons['try $subgoals%42%2])
...
($arglist%4n%2 cons['try $subgoals%4n%2]))]
%1thus, by %2Sublemma 4.1
bktrkcond[actuals, (($arglist%41%2 (cons 'try $subgoals%41%2))
($arglist%42%2 (cons 'try $subgoals%42%2))
...
($arglist%4n%2 (cons 'try $subgoals%4n%2)))] = %7s%2
∧ %7s%2 ≠ undef
≡
∃i match[actuals, newversion[$arglist%4i%2]] = %7s%4i%2 ∧ %7s%4i%2 ≠ undef
∧ try[$subgoalist%4i%2%7s%4i%2] = %7s%4i%9'%2 ∧ %7s%4i%9'%2 ≠ undef
∧ %7s%2 = cleanup[%7s%4i%fo%7s%4i%9'%2, actuals] ∧ %7s%2 ≠ undef
%9∧%6↑[i-1]&↓[#j=1]%2# ¬(match[actuals,newversion[$arglist%4j%2]] =%7s%4j%2
∧ %7s%4j%2 ≠ undef ∧ (try[$subgoalist%4j%2%7s%4j%2] = %7s%4j%9'%2
∧ %7s%4j%9'%2 ≠ undef) )
≡
∃i match[actuals, newversion[$arglist%4i%2]] = %7s%4i%2 ∧ %7s%4i%2 ≠ undef
∧ try[$subgoalist%4i%2%7s%4i%2] = %7s%4i%9'%2 ∧ %7s%4i%9'%2 ≠ undef
∧ %7s%2 = cleanup[%7s%4i%fo%7s%4i%9'%2, actuals] ∧ %7s%2 ≠ undef
%9∧%6↑[i-1]&↓[#j=1]%2# ( (match[actuals,newversion[$arglist%4j%2]] =%7s%4j%2
∧ %7s%4j%2 ≠ undef) → ¬(try[$subgoalist%4j%2%7s%4j%2] = %7s%4j%9'%2
∧ %7s%4j%9'%2 ≠ undef) )
%1 by %2Lemma 2%1 we know
%2unify[actuals, $arglist%4i%2] = %7s%4i%2
≡ match[actuals, newversion[$arglist%4i%2]] = %7s%4i%2 ∧ %7s%4i%2 ≠ undef
%1 by %2Lemma 3,%1 we have
%2S[%3$subgoals%2] ≡ try[$subgoals] = %7s%2 ∧ %7s%2 ≠ undef
thus, we have
%2 ∃i ( unify[$id-list, $arglist%4i%2] = %7s%4i%2
∧ %9∧%6↑[i-1]&↓[#j=1]%2#(unify[$id-list, $arglist%4j%2] = %7s%4j%2 → ¬%2S[%3$subgoals%4j%2%7s%4j%2])
∧ %9∧%2(subgoalist%4i%2)%7s%4i%2 )
≡
bktrkcond[actuals, (($arglist%41%2 (cons 'try $subgoals%41%2))
($arglist%42%2 (cons 'try $subgoals%42%2))
...
($arglist%4n%2 (cons 'try $subgoals%4n%2)))] = %7s%2
∧ %7s%2 ≠ undef
.indent 70,0,0
QED
.end
.begin nofill;turn on "↑[]&↓"
%2THEOREM (Correctness of LISP form)
%2∀%g¬%2x defined[ inputs[$id-list, $input-pattern] ] ∧ $precondition →
[ ∃i ( unify[$id-list, $arglist%4i%2] = %7s%4i%2
∧ %9∧%6↑[i-1]&↓[#j=1]%2#(unify[$id-list, $arglist%4j%2] = %7s%4j%2 → ¬%2S[%3$subgoals%4j%2%7s%4j%2])
∧ S[%3$subgoals%4i%2%7s%4i%2] )
→ ($id-list)%7s%4i%2 ε $name) ]
∧
∀%g¬%2x [($id-list ε $name) → $postcondition]
≡
%2∀%g¬%2x [ true-precond[(cons $name actuals)]
∧ bktrkcond[actuals, (($arglist%41%2 (cons 'try $subgoals%41%2))
($arglist%42%2 (cons 'try $subgoals%42%2))
...
($arglist%4n%2 (cons 'try $subgoals%4n%2)))] = %7s%2
∧ %7s%2 ≠ undef
→ (actuals)%7s%2 ε $name ]
∧ %2∀%g¬%2x [(actuals ε $name) → $postcondition]
.end
.fp
%1Proof:
.begin indent 10,6,6
The proof has actually all been accomplished through the lemmas. We take it as
obvious that the second conjunct of the first expression is equivalent to the
second conjunct of the second expression. Lemmas 1 and 4 supply the necessary parts to
put together the equivalence of the first conjuncts of each expression.
.end
.sec(Adding a New Target Language,,,P17:)
In this section we describe how to add a new target language to the system. The
first and most important step is to choose an implementation strategy.
One has a great deal of flexibility at this point. A balance must be found between
compatibility with the full power of the specification language and with
programs written directly in the target language. The main objective is to
generate correct programs in the target language - not to extend or re-define
the capabilities of that language. We would like the programs written from
their specifications to be able to interact in well-defined and convenient
ways with programs written directly in the target language.
If the target language distinguishes functions from procedures, then it may
be preferable to use procedures as the implementation of all functions.
In this way the variable bindings are simply a side effect of the computation,
which is the way it happens in logic anyway. If one wanted to stay close to
logic, all functions would be implemented as boolean functions.
Once a strategy
has been decided upon the following functions/procedures should be implemented.
All of these definitions are to reside in the target language system except
for %3make_(language name)_def%1 and %3autopred%1. These two functions are meant
to be added to the program generation system. The only change to be made in the
system is in the function %3translate%1. For type-free languages, the clause
%3((eq target 'language) (make_language_def))%1 is added; for typed languages,
the clause %3((eq target 'language) (mk-strong-typed) (make_language_def))%1 is
added.
.fp
1. Primitives:
The functions and predicates listed here are labeled "primitives"
because we assume they need not be further defined. The set of primitives given
here is neither minimal nor exhaustive, just convenient. One's target language
may supply more than these, or less.
If one supplies more primitive types for a
strong-typed language, then the system must be informed of those type names.
This may be accomplished by type specifications with empty bodies, i.e. when
asked for the body part of the specification, simply type a period. Note that this
is only for type definitions, and only for strongly-typed languages. For type-free
target-languages, and for all other function definitions, if one wishes to make
use of a function or predicate already defined in the target language, then one
should use the "%3∩f%1" or "%3∩p%1" facility (see {yon (P7)}).
If a target language is unable to supply some of the following primitives, one
may still use the system, but should not make use of those undefined primitives
in any specifications.
.begin indent 5,10,10;single space
.pt24
a. Predicates - primitive predicates do not have an output variable.
They are defined in the target language such that they always
take true or false as value, in type-free languages, and, if
the language is typed then they must either be primitive or defined
types in that language. Occurrences of these type predicates
in preconditions and postconditions will simply become declarations
in a typed target-language.
.begin nofill;turn on "↑"
Integer(x)
Real(x)
Boolean(x)
Is-String(x)
Is-List(x)
binary relational predicates: =, ≠, >, <, ≥, ≤
(I/O): Firstsym(x y z) - meaning y is the first symbol, i.e.token,
of x, leaving z.⊗↓The specification of the system
is done in such a way that %3Firstsym(x, y, z)%1 could simply be implemented as a
scanner which gets the first token of input, binds it to %3y%1, and ignores %3x%1
and %3z%1. %3Firstsym%1 with three arguments indicates unlimited backtracking
abilities over input. Since this is not always implementable in one's target
language, one must use the general form judiciously. Similarly with %3Firstexp%1.←
Firstexp(x y z) - meaning y is the first expression on x,
leaving z, where
expression ::= constant | variable |"(" expression↑* ")"
Write(x) - has the value true for all x, and has the side
effect of printing the value of x on the current output
device.
.end
.pt24
b. Functions - these are functions whose application to arguments result
in terms. Thus, they do not carry output variables. The predicate-ized
.begin turn off "%"; turn on "{}"
version of any of these (see {yon P7}) is obtained by preceding the name
with "%f"
.end
.begin nofill
(Integer): +, -, *, /, rem
(Real): r+, r-, r*, r/
(Boolean): ∧, ∨, ¬
(String): string(l)-makes a string out of a list of characters
s-cat(s1 s2) - string concatenation
s-cons(c s) - adds a character to the front of a string
firstch(s) - gets the first character of a string
tail(s) - rest of a string (without first character)
mk-string(c) - makes a string of a single character
(List): first(l) - gets first element of a list l
rest(l) - gets the list l without the first element
cons(x l) - adds x to front of list l
list(x1 ... xn) - creates a list with elements x1 ... xn
.end
.pt24
c. Constants - the grammar for the intermediate form describes the constants
of the system, and of course any mapping to another language must
be able to recognize constants. The reason we mention them here
specifically, is that we have included at least one constant that
is not universally available in typical programming languages.
This constant is of course %3undef%1. It may not be convenient
(or even possible) to introduce such a constant in strongly typed
languages. However, the purpose of %3undef%1, i.e., some way of
indicating that we have determined that a well-defined value in
the appropriate domain does not exist, should be implemented.
More is said about this in the section on implementing
strongly-typed languages.
.end
.begin indent 0,0,0;single space
.pt24
2. The following functions must also be implemented. The first, %3make_(language name)_def%1,
should be an actual function or procedure name. The others are indicative of
what needs to be accomplished. They need not exist as explicitly defined functions.
For example, the target language does not need to have a procedure named %3bktrkcond%1,
however, the function of %3bktrkcond%1, i.e., the selection of alternatives to
attempt in order to complete a computation, must be accomplished by some means.
.end
.begin indent 6,10,10;single space
.pt24
a. %3make_(language name)_def%1 - This function has available all the
information of the intermediate language definition. It creates the
target language definition, i.e., the actual syntax of a procedure
declaration/definition in the target language.
.pt24
b. %3bktrkcond%1 - This function may be accomplished as an ordinary conditional, allowing
several options, or as a sequence of IF-THEN-ELSE's with added conditions
to ensure completion of only one alternative.
.pt24
.begin indent 15,20,20
1) %3undef%1 - A distinguishable bottom element of every type is used
as an undefined element. Languages that are strong-typed without the
ability to add a single element to an existing type cause
trouble here. In these cases, a variable %3undef%1 may be used
which is local to each %3bktrkcond%1 and passed through to %3try%1.
.end
.pt24
c. %3match%1 - The pattern match may simply be a unification algorithm;
a more general matcher will allow more complicated input to the matcher,
and thus enhance the system's efficiency if done well. A simple unification
algorithm is guaranteed to be correct, but requires that one must only
desire syntactic matching. That is, the matcher would not be able handle
the unification of any data types that have more than one representation.
.pt24
d. %3try%1 - The function %3try%1 attempts to complete the computation of a list of procedure
calls. If any call is unsuccessful, then %3try%1
fails, and another alternative is selected by %3bktrkcond%1.
.pt24
e. a precondition checker - This may be implemented
as a type check and/or first condition of the procedure body, governing
the execution of the rest of the body.
.end
.begin indent 0,0,0;single space
.pt24
Each of the functions mentioned above may require several subfunctions.
For example, in a typed language one would probably split
%3make_(language name)_def%1 into sub-parts such as %3make_dec_part%1
and %3make_body_part%1.
One also needs to check whether the lexicon of the intermediate language
is compatible
with the lexicon of the target language, and provide a mapping from one
to the other if they are not. Of particular concern here is the fact that
the %3autopred%1 facility allows identifiers whose first characters are
the symbol %3∩%1 and the internalized form of the formal parameters are
identifiers with first symbol "!".
.pt24
.fp
3. Define %3autopred%1 to allow use of language-system-defined functions and
procedures (see {yon P7}). Also helps in the automatic predicatizing of the primitive "functions"
mentioned in step 1.
.end
.ss(Implementation Strategy for LISP)
The definitions of the primitives for LISP are given in {yonss (P13)}, beginning
on {yon (P9)}. The choice of an implementation strategy was changed after seeing
the results in the first implementation of LISP. We discuss this here since
it the lesson learned in the process may be applicable to several languages.
Every function call in most implementations of LISP returns a single value.⊗↓See
%3Anatomy of LISP%1 [A 78] for a discussion of an implementation of LISP with
multiple-valued functions.← Thus, in the original
implementation it was thought that to be consistent with LISP every function
call should return the value of its output variable. This decision seemed
quite natural at first, in fact it seemed the only way to be compatible
with ordinary LISP.
No problems arose as long as the functions being defined had precisely one
output variable.
It somehow seemed reasonable to
expect that one should only want to compute a single value when dealing
with a language in which that is the norm.
However, when faced with a function having two or more
output variables, one had to choose which was to be the value returned.
The arbitrary choice was made that the first output variable would carry
the value returned by the function call. Although somewhat dissatisfying
this choice caused no major problems, immediately.
The point at which the strategy was found to be inadequate came
when implementing the propagation of the values of the output variables
to the rest of the current list of subgoals. It was certainly possible
to do this, but it was not pretty.
A new strategy was chosen. Each function call would return a substitution.
This strategy is completely compatible with LISP in that a substitution is
indeed a single value. It was still easy to automatically generate
"predicate-ized" versions of LISP-system functions.
The new implementation turned out to be much cleaner and more amenable
to proof than the old. The lesson to be learned from this is that there
are usually many possible choices of implementation strategy, one should
not feel stuck with the first choice, and one should not overly restrict
the implementation by avoiding what may at face value appear to be an
extension of the target language, but in fact is not.
.ss(Implementation of Pascal)
In any typed language, some additional information about the types of
parameters and local variables is desired, and it is convenient to
generate this information once and keep it where one can continually reference
it. When it is recognized that a program is to be generated in a strongly
typed language we add more information to the property list of the function
being defined.
A list of the formal parameters and their types is put under the property
%3types%1. These types are gleaned from the precondition and postcondition
specifications. The remainders of the precondition and postcondition (i.e.
that which is in addition to type specifications) are listed on the
%3typedprecond%1 and %3typedpostcond%1 properties of the function.
The body of the function is searched to determine the names of all functions
that are called by the function being defined, and this list of names
is stored under the %3external-procs%1 property. A list of the local
variables and their types is generated and stored under the %3local-decs%1
property. When an external declaration is made for a function, it is also
kept so that the same declaration need not be derived again for every other function
that calls it.
In Pascal, a function or type
specification is implemented as a boolean function with value
parameters corresponding to the input parameters and %3var%1 parameters
corresponding to the output parameters. A function will return the value
%3true%1 if it is successful and %3false%1 if it is not. All user-defined
types are treated as one type, and functions are generated to distinguish
among them.
If one wishes to translate to
Pascal, or any strongly typed language, part of the precondition must
be a type specification for each input parameter, and part of the postcondition
must be a type specification for each output parameter.
This means that there may be
some specifications that are legal input to the system that will not
be translatable into Pascal.
The necessary additions to the system for implementing Pascal as a target
language may be found in {yonss (P14)}, {yon (P12)}.
Appendix A, which contains several sample specifications and their translations
into LISP programs, exhibits only one generated Pascal program. This is due
to the extreme ugliness of the implementation of the "back end" for Pascal.
To satisfy the type restrictions of Pascal we had to either disallow user-defined
types or map all types to a general type (we used "term").
Mapping all types to one results in a very general structure. This structure
is nice theoretically in its universality, but unwieldy in practice. We felt the
point could be shown by exhibiting the translation of the factorial function.
The full generality of the structure is used even for this simple example, and
we are unable to simplify it for the cases in which we are only dealing with
the base types of Pascal. The primitive functions and predicates are defined
to take advantage of the operations possible on base types; however, this is
because the primitives are implemented by hand and can be designed individually.
In conclusion, the implementation of Pascal has shown that strongly-typed
languages may be added to the system; however, if the system is to be
considered for "practical" use, an implementation that encodes types more
efficiently should be investigated.
.sec(Implementation Notes)
The top level of the system is called "top" and is called by typing "(top)"
to MACLSP.
When the program is initialized it prompts the user suggesting
that if help is needed one should type "?". This results in instructions
for input specifications. The system prompts the user for individual parts of
a specification, and again a "?" response will provide
information about the required specification, along with an example.
When the user terminates a session, by typing "." at the top level, the system
asks if one wishes to save the definitions of the session on a file, and asks for
a filename if the answer is affirmative. Before terminating the session, the system
informs the user how to include the definitions just saved the next time the system
is started.
The pattern-matcher plays an important part in the computation of programs.
Alternatives in the backtracking-conditional are chosen by matching the actual
parameter list against a pattern. A straight unification algorithm is easy to
implement but not always as powerful as we would like. It works well where
there is a unique representation of the objects we are trying to match. If
one chooses to define a data type in which the representation for each element is not
unique, then one should also define an equality predicate "%3Equal-<type>%1"
for the type, and if one desires more than syntactic matching to occur, a function
"%3Equal-bind-<type>%1" that will attempt to match two elements of the type.
All other equality testing and matching is done syntactically.
For example, if one chose to represent sets as unordered constructions rather than
imposing some order, one might provide the following specifications:
.begin "ex" nofill;select 3
type Set
body? Set(Mt-set, true)
Set( Add-elem(y,X), true) ← Set(X, true), Member(y, X, false).
function Equal-set
input-pattern? (1 1 0)
parameter-list? (x y z)
precondition? Set(x, true) ∧ Set(y, true).
postcondition? Boolean(z, true).
body?
Equal-set(x, y, true) ← Subset(x, y, true), Subset(y, x, true).
.end "ex"
.fp
Of course, "%3Subset%1" and "%3Member%1" must also be defined.
Note the use of %3false%1 in the second clause of the specification of the body
of %3Set%1. Negation of predicates is not allowed by the syntax of Horn clauses;
using a truth-valued output variable we are able to incorporate negative tests
into the language. In the definition of %3Member%1 we would have a clause:
%3Member(x, (), false) ← %1.
The %3true%1 or %3false%1 used as an argument of a predicate must be considered
a constant (or 0-ary function symbol) not a predicate. When using the constant
predicate, %3TRUE%1 or %3T%1, we distinguish it here by capitalization. The user
should be aware of the distinction, however, it is not necessary to communicate
it to the system through capitalization since the distinction can be determined
by context.
Failure to find an answer will cause the value %3undef%1 to be returned. This is
an indication that the answer is undefined either because we attempted to apply
a predicate to arguments not in its domain (as specified by the precondition) or
we failed to match on all of the clauses of the definition. Returning
%3undef%1 will fail the subgoal it is returned to and thus fail the current clause
and the next alternative will be attempted. At this level, %3undef%1 is denoting
failure to successfully terminate a computation.
At another level, %3undef%1 is a constant that is assumed to be in every domain.
It is possible that one might
call a subgoal with the constant %3undef%1 in an output variable position;
in this case, if %3undef%1 is the value that would be bound to that position,
then the subgoal will succeed. There are times when %3undef%1 is the appropriate
answer to be returned from a function. For example, if one defines a look-up
function that takes a name and a list of name-value pairs, and returns the value
associated with the name, then one would expect an output value %3undef%1 if the
name does not occur in the list.
The system will provide default values for the parameter-list, precondition, and
postcondition of the specification of a function as it does for a type specification.
This makes the input of specifications easier but is not recommended
for general use. Even when specifying a program that is only expected to be
partially correct, one should be able to provide a precondition that would at
least keep %2some%1 bad inputs from being accepted.
.P7:
A further convenience for the user, the system will automatically "predicate-ize"
functions that are pre-defined in the target-language system. The user indicates
such functions to the synthesis system by prefixing the name of a function with
"%3∩f%1" and the name of a system predicate (boolean valued function)
with "%3∩p%1".
An output variable is added to the argument list and the new predicate may
be used as any other. For example, the recursive clause for the definition of
factorial:
.begin center;select 3
fact(x, y) ← ∩fsub1(x, x1), fact(x1, y1), ∩f*(x, y1, y)
.end
.fp
makes use of the system functions "%3sub1%1" and "%3*%1". Again, since these are
being defined automatically, the preconditions are simply "true", so the only
type checking done will be that provided by the target language. We
do not guarantee correctness for definitions made in terms of system functions.
The mapping to a strongly-typed language requires that more detail be spelled
out. When the system recognizes that the target language
requires explicit declaration of types, it derives from the specifications
some additional properties that will be useful in the translation.
These include a list of formal parameters associated with their types, a
list of local variables and their types, and a list of all functions that
are called by the one being specified.
.sec(Conclusions and Further Research)
We have shown, through proofs of the correctness of the mappings involved,
that the system described in this document provides a valid way
of generating correct programs. The system works by adding control information
to the logic that is specified by the user. The user is still left with
the task of inventing the computational logic description of the program
desired. We feel that this is reasonable and an advance in the process of
obtaining a correct program since the programmer is no longer burdened with
the problem of describing the flow of control of the program.
The system as described is "reasonably" target-language-independent. We qualify
this statement only because it is easier to translate to some languages than
to others. For ease of translation, the target language should allow recursion.
The "back-end" necessary to translate to a non-recursive language, although
certainly feasible, would be more complicated than that for a language
allowing recursion due to the necessity
of translating recursive algorithms. We feel this is almost no restriction
at all since we believe that recursion is important enough to be a minimum
requirement for any language to be considered "reasonable".
The type structure of a target language is an important factor in determining
the ease of its addition to the system. The simplest languages to deal with
are those that are type-free, allowing type specifications to be translated
into functions that are recognizers for the type being defined. In a typed
language, one often feels the need (or desire) for polymorphic functions as
allowed by LCF. LCF checks the consistency of types without insisting on
knowing precisely the type of every object at compile time. For example,
one can define the function %3compose%1, which takes two arguments of functional
types and returns a value of functional type. The type assigned to %3compose%1
by LCF is:([type2 → type3] X [type1 → type2]) → [type1 → type3]. A simple
example of another function that is by nature polymorphic is a symbol table
lookup. The type of the result of a lookup should agree with the type of
the variable the function is called with. However, there may be several
different types of variables and values in the table at any time.
The use of generic functions in the specifications
is a new feature making it possible to synthesize
several programs from a single specification.
Generic functions also provide a convenient tool in defining other functions.
The portability of the system is evidenced by its ability to generate a
version of itself.⊗↓The version of the system which was generated from the
specification given in {yonsec (P15)} is slow in comparison to the hand-written
version. We believe this is largely due to the simple-minded pattern matcher
being used, which makes actual substitutions rather than simulating them with
binding of variables. This is actually a problem with the implementation
of %3match%1 written directly in LISP rather than a problem with the specification.←
Thus it is easily bootstrapped given the "back-end"
for the language desired. The ability to generate itself is also an
indication that the system can handle large "practical" problems. Several sample
programs have been generated, many are listed in Appendix A.
Several extensions to the system and subjects of further research have
suggested themselves along the way. We divide these loosely according to whether
they deal with the front-end of the system, the present capabilities of the system,
or the back-end required to add a new language.
We would like to add a front-end to the system that would allow more natural input.
This includes several extensions of the syntax of the specification language.
First, the use of embedded function applications cuts down on the amount of
typing necessary. We can trivially make use of
function applications that have only a single output variable
by a simple syntactic manipulation that replaces the occurrence of these in argument
positions by a temporary variable and adds the function application, with that
same variable in the output position, to the subgoals of the clause in which
it occurs before sending the input to the system. If we are also to include
functions that have not yet been defined, then we must have a way of distinguishing
them from constructor functions⊗↓Constructor functions are
used to define data structures inductively.
For example, the definition of type %3Set%1 given on {yon (P11)} uses the
constructor function %3Add-elem%1.←
, which must never be turned into predicates.
This is not difficult and can be done in any of a number of ways.
Secondly, we can extend the syntax of Horn clauses to allow mixed conjunctions
and disjunctions of positive literals (still no negation allowed) on the right
hand side of the "←".
Thirdly, it would be nice to allow full use of Predicate Calculus in the
specification of a function. This is a much more difficult problem. Synthesis
of programs from general descriptions is being studied by several researchers
([C 77], [CD 78], [CS 77], [D 75], [D 77], [DM 75], [MW 77a], [MW 77c]).
Hopefully, their results may be incorporated in this system in the future.
Brian Beach, a student at the University of California, Santa Cruz, has implemented
an interactive system that helps one derive Horn clauses from more general
statements in Predicate Calculus [B 79].
Lastly, we would like to include an interactive program that helps the user
derive the specifications for a program and prove the correctness of the
specifications. The system could check the completeness of the specification
by making sure that at least one Horn clause is applicable to every element
of the domain of the function as specified by the precondition. This is
difficult in general but for inductively defined domains may simply be a
reminder to the programmer that they include basis and constructed elements.
To prove the correctness of a specification one must: 1)Prove each
Horn clause as a theorem in the problem domain; 2) Prove that the precondition
guarantees termination of the program (usually a proof by induction on the
input); and 3) Prove that successful termination of the program always results
in an answer satisfying the postcondition, and that the answer produced is
unique. This is then a proof that we have a correct specification of %3a%1
problem; again, we can never prove it is the problem we had "in mind".
It is of course too much to expect that the system be capable of
doing all of this on its own, but a semi-automatic verifier or proof checker
would be useful.
There are also several extensions to the capabilities of the system that are
desirable. We would like to extend the use of generic function specifications
to allow selection of individual versions of the function by type of the
arguments as well as by input pattern. Another useful feature would be
obtained by making arrays a primitive data type. Array access is not
achieved efficiently by a logic program; since most available languages
offer arrays as a primitive type, we could make use of them in specifications
realizing that the fast index algorithms of a target language would eventually
be used by the program.
Functional arguments are disallowed
in any first-order theory, however, we could circumvent the jump to second
order and its associated problems by considering the use of function names
as arguments. These names could then indicate where we might find the
appropriate definition of the function we wish to use.
Another restriction
we have imposed is the functionality of our specifications. This gave a
great savings in terms of the limited backtracking needed for evaluation
(over clauses, but never over subgoals). We would like to include a
way of indicating that selective subgoal backtracking is desired. This
would give us the ability to make statements about the existence of an answer
that satisfies several subgoals simultaneously. Each subgoal may be satisfied
by a set of answers, we want an element of the intersection of these sets.
There are several ways of improving the efficiency of the generated programs.
We intend to incorporate some analysis to determine the best ordering of
alternatives and of subgoals within alternatives.
We would also like to generate programs to optimize the source language programs
for particular target languages. In languages in which recursion is implemented
inefficiently, this would include removal of recursion.
The most dramatic improvement to the system would be the development of a
program that could automatically generate the mapping from intermediate to
target language from a formal specification of the syntax and semantics
of the target language. This is similar to the work being done on
translator writing systems, the difference being that the target
is a high level programming language rather than a machine language.
.bib;
.begin "bib" indent 0,16;single space;turn on"\#";tabs 12
.AT NULL ⊂IF FILLING THEN BREAK ELSE SKIP 1⊃;
.fp
[A 78]\#Allen, J. R.,%3Anatomy of LISP%1. McGraw-Hill Publishing Co.,
New York, New York, 1978.
.pt24
.fp
[AN 76]\#Andreka, H. and I. Nemeti, "The Generalised Completeness of Horn
Predicate-Logic as a Programming Language", D.A.I. Research
Report No. 21, Department of Artificial Intelligence, University
of Edinburgh, March, 1976.
.PT24
.fp
[B 57]\#Backus, J. W., R. J. Beeber, S. Best, R. Goldberg, L. M. Haibt,
H. L. Herrick, R. A. Nelson, D. Sayre, P. B. Sheridan,
H. Stern, I. Ziller, R. A. Hughes, and R. Nutt, "The
FORTRAN Automatic Coding System", %3Proceedings of the
Western Joint Computer Conference%1, vol. 11, 1957.
.pt24
[BGW 77]\#Balzer, R. M., N. M. Goldman, and D.S. Wile, "Informality in
Program Specifications", University of Southern California
Information Sciences Institute, ISI/RR-77-59, April, 1977.
.pt24
[B 77]\#Bauer, F. L., H. Partsch, P. Pepper, and H. W%9:%1ossner, "Notes on the Project
CIP: Outline of a Transformation System", TUM-INFO-7729,
Institut Fur Informatik, Technische Universit%9:%1at M%9:%1unchen,
July, 1977.
.pt24
[B 79]\#Beach, B., "Transforming Predicate Calculus Statements Into Horn Clauses",
(tentative title), Senior Thesis, University of California,
Santa Cruz, June, 1979.
.pt24
[BK 76]\#Biermann, A. W., and R. Krishnaswamy, "Constructing Programs From
Example Computations", %3IEEE Transactions on Software Engineering%1,
vol. 2, no. 3, Sept., 1976.
.pt24
[B 74]\#Buchanan, J. R., "A Study in Automatic Programming", AIM-245, STAN-CS-74-458,
Ph.D. Thesis, Stanford University, May, 1974.
.pt24
[BL 74]\#Buchanan, J. R., and D. C. Luckham, "On Automating the Construction of Programs",
SAIL AIM-236, STAN-CS-74-433, Stanford University, May, 1974.
.pt24
[BD 75]\#Burstall, R. M., and J. Darlington, "Some Transformations for Developing
Recursive Programs", %3Proceedings of the International Conference
on Reliable Software%1, Los Angeles, Ca., 1975.
.pt24
[BD 76]\#Burstall, R. M., and J. Darlington, "A Transformation System for Developing
Recursive Programs", D.A.I. Research Report No.19,
University of Edinburgh, March, 1976.
.pt24
[C 78]\#Clark, K., "Negation as Failure", in %3Logic and Data Bases%1 (H. Gallaire
and J. Minker, Eds.), Plenum Press, New York, N.Y., 1978.
.pt24
[C 77]\#Clark, K., "Synthesis and Verification of Logic Programs", Research report,
CCD, Imperial College, 1977.
.pt24
[CD 78]\#Clark, K., and J. Darlington, "Algorithm Classification Through Synthesis",
Imperial College of Science and Technology, London, June, 1978,
to appear in %3Computer Journal%1.
.pt24
[CS 77]\#Clark, K., and S. Sickel, "Predicate Logic: A Calculus for Deriving
Programs", %3Proceedings of the Fifth International Joint Conference
on Artificial Intelligence%1, Cambridge, Mass., Aug., 1977.
.pt24
[D 75]\#Darlington, J., "Applications of Program Transformation to Program
Synthesis", %3IRIA, Proceedings of the Symposium on Proving
and Improving Programs%1, Rocquencourt, France, 1975.
.pt24
[D 77]\#Darlington, J., "Program Transformation and Synthesis: Present Capabilities",
DAI Report No. 48, University of Edinburgh, Research Report No. 77/43,
Imperial College of Science and Technology, Dept. of Computing and
Control, Sept., 1977.
.pt24
[DB 76]\#Darlington, J., and R. M. Burstall, "A System Which Automatically Improves
Programs", %3Acta Informatica%1, vol. 6, pp.41-60, 1976.
.pt24
[D 78b]\#Davis, R. A., "Minis vs. Micros: OEM Decision-Making Risks Grow",
%3Digital Design%1, vol. 8, no. 8, Aug., 1978.
.pt24
[D 76]\#Davis, R. E., "Deduction, Truth, and Computation", Master's Thesis,
San Jose State University, San Jose, Ca., 1976.
.pt24
[DM 75]\#Dershowitz, N., and Z. Manna, "On Automated Structured Programming",
%3IRIA, Proceedings of the Symposium on Proving
and Improving Programs%1, Rocquencourt, France, 1975.
.pt24
[E 78]\#van Emden, M. H., "Computation and Deductive Information Retrieval", in
%3Formal Description of Programming Concepts%1, (E. Neuhold, Ed.),
North Holland, 1978.
.pt24
.fp
[EK 74]\#van Emden, M. H., and R. A. Kowalski, "The Semantics of Predicate Logic
as a Programming Language", Memorandum MIP-R-103, School of
Artificial Intelligence, University of Edinburgh, Feb., 1974.
.pt24
[F 79]\#Franusich, M., "Analysis of Logic Programs for Static and Dynamic Subgoal
Selection", Senior Thesis,
University of California, Santa Cruz, June, 1979.
.pt24
[G 75]\#Gerhart, S. L., "Correctness-Preserving Program Transformations", %3Proceedings
of the 2nd ACM Symposium on Principles of Programming Languages%1,
pp.54-66, January, 1975.
.pt24
[GBW 78]\#Goldman, N. M., R. M. Balzer, and D. S. Wile, "The Inference of
Domain Structure from Informal Process Descriptions", %3Proceedings
of the Workshop on Pattern-Directed Inference Systems%1,
Honolulu, May, 1978.
.pt24
[G 77]\#Green, C. C., "A Summary of the PSI Program Synthesis System",
%3Proceedings of the Fifth International Joint Conference on
Artificial Intelligence%1, Cambridge, Mass., August 1977.
.pt24
[H 75a]\#Hardy, S., "Synthesis of LISP Functions from Examples", %3Proceedings of
the Fourth International Joint Conference on Artificial
Intelligence%1, Tbilisi, Georgia, U.S.S.R., Sept., 1975.
.pt24
[H 76]\#Heidorn, G. E., "Automatic Programming Through Natural Language
Dialogue: A Survey", %3IBM Journal of Research and Development%1,
vol. 20, no. 4, July, 1976.
.pt24
[H 75b]\#von Henke, F., "On Generating Programs from Data Types: An Approach
to Automatic Programming",
%3IRIA, Proceedings of the Symposium on Proving
and Improving Programs%1, Rocquencourt, France, 1975.
.pt24
[H 79]\#von Henke, F., "Pascal Unifiers", unpublished manuscript, 1979.
.pt24
[ILL 75]\#Igarashi, S., R. L. London, and D. C. Luckham, "Automatic Program
Verification I: A Logical Basis and its Implementation",
%3Acta Informatica%1, vol. 4, pp. 145-182, 1975.
.pt24
[JW 74]\#Jensen, K., and N. Wirth, %3Pascal User Manual and Report%1, second
edition, Springer-Verlag, New York, N.Y., 1974.
.pt24
[K 52]\#Kleene, S. C.. %3Introduction to Metamathematics%1. Van Nostrand
Company, Inc., Princeton, N.J., 1952.
.pt24
[K 74]\#Kowalski, R., "Predicate Logic as Programming Language", %3Proceedings
IFIP 74%1, North-Holland Publishing Company, 1974.
.pt24
[LC 74]\#Lee, R. C. T., and S. K. Chang, "Structured Programming and
Automatic Program Synthesis", %3Proceedings of a Symposium on
Very High Level Languages%1, Santa Monica, Ca., 1974.
.pt24
[L 75]\#Lenat, D. B., "Synthesis of Large Programs from Specific Dialogues",
%3IRIA, Proceedings of the Symposium on Proving
and Improving Programs%1, Rocquencourt, France, 1975.
.pt24
[L 77]\#Loveman, D. B., "Program Improvement by Source-to-Source Transformation",
%3Journal of the ACM %224:1%1, pp.121-145, 1977.
.pt24
[L 73]\#Lukasik, S. J., Testimony to House Armed Services Subcommittee,
USGPO, pp.3509-3559, June, 1973.
.pt24
[MW 77a]\#Manna, Z. and R. Waldinger, "The Automatic Synthesis of Recursive Programs",
%3Proceedings of the Symposium on AI and Programming Languages%1,
SIGPLAN/SIGART NOTICES/NEWSLETTER Vol. 12, No. 8, August, 1977/
No. 64, August, 1977.
.pt24
[MW 77b]\#Manna, Z. and R. Waldinger, "The Logic of Computer Programming", AIM-298,
STAN-CS-77-611, Stanford University, August, 1977.
.pt24
[MW 77c]\#Manna, Z. and R. Waldinger, "Synthesis: Dreams => Programs", AIM-302,
STAN-CS-77-630, Stanford University, November, 1977.
.pt24
[MT 79]\#McCarthy, J., and C. Talcott, %3LISP Programming and Proving%1.
To be published.
.pt24
[M 64]\#Mendelson, E., %3Introduction to Mathematical Logic%1. D. Van Nostrand
Company, Inc., Princeton, New Jersey, 1964.
.pt24
[M 74]\#Moon, D., %3MACLISP Reference Manual%1, Project MAC, Massachusetts
Institute of Technology, Cambridge, Massachusetts, 1974.
.pt24
[S 77a]\#Sickel, S., "A Logic-Based Programming Methodology", Technical Report
no. 77-8-001, Univesity of California, Santa Cruz, March, 1977.
.pt24
[S 78]\#Sickel, S., "Invertibility of Logic Programs", Technical Report No. 78-8-005,
University of California, Santa Cruz, August, 1978.
.pt24
[S 65]\#Slagle, J. R., "Experiments with a Deductive Question-Answering Program",
%3Communications of the Association for Computing Machinery%1, Vol. 8,
No. 12, Dec., 1965.
.pt24
[S 74]\#Standish, T., "ARPA's Automatic Programming Research: A Quest for a
Coherent View", (draft), Feb., 1974.
.pt24
[S 77b]\#Summers, P. D., "A Methodology for LISP Program Construction from Examples",
%3Journal of Association for Computing Machinery%1, vol. 24, no. 1,
Jan., 1977.
.pt24
[W 69]\#Waldinger, R. J., "Constructing Programs Automatically Using Theorem
Proving", Ph.D. Thesis, Department of Computer Science,
Carnegie-Mellon University, Pittsburgh, Pa., May, 1969.
.pt24
[WBG 77]\#Wile, D. S., R. M. Balzer, and N. M. Goldman, "Automated Derivation
of Program Control Structure from Natural Language Program
Descriptions", %3Proceedings of the Symposium on Artificial
Intelligence and Programming Languages%1, University of Rochester,
N.Y., Aug., 1977.
.pt24
[UM 77]\#Ulrich, J. W., and R. Moll, "Program Synthesis by Analogy",
%3Proceedings of the Symposium on Artificial
Intelligence and Programming Languages%1, University of Rochester,
N.Y., Aug., 1977.
.pt24
.end "bib"
.sec(Appendix A: Sample Specifications)
.begin nofill;select 3;tabit1(50)
type Nat
body? Nat(x true) ← Integer(x true), ≥(x 0 true).
(DEFUN NAT FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'NAT L))
(BKTRKCOND L
'(((!X T) (TRY (INTEGER !X T) (≥ !X 0 T))))))
(T 'UNDEF)))
generic add
parameter list? (x y z)
choices?
(1 1 0)
function name? ∩f+\%1since %3∩f+ %1is a function
%3choices?\%1already known to the system, no
%3(1 0 1)\%1further information is required
%3function name? add-2
precondition? Integer(x) ∧ Integer(z).
postcondition? Integer(y).
body-name? sub-2
choices?
(0 1 1)
function name? add-1
precondition? Integer(y) ∧ Integer(z).
postcondition? Integer(z).
body-name? sub-1
choices?
.
body-defs:
sub-2?
add(x y z) ← ∩f-(z x y).
sub-1?
add(x y z) ← ∩f-(z y x).
(PUTPROP 'ADD '(((1 1 0) . ∩F+) ((1 0 1) . ADD-2) ((0 1 1) . ADD-1)) 'GENERIC)
(DEFUN ADD-2 FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'ADD-2 L))
(BKTRKCOND L
'(((!X T) (TRY (INTEGER !X T) (≥ !X 0 T))))))
(T 'UNDEF)))
(DEFUN ADD-1 FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'ADD-1 L))
(BKTRKCOND L
'(((!X T) (TRY (INTEGER !X T) (≥ !X 0 T))))))
(T 'UNDEF)))
END_OF_GENERIC_SPEC
generic imult\%1Integer multiplication, the result will
%3parameter list? (x y z)\%1be an integer, or %3undef if there
%3choices?\%1is no integer meeting the semantics.
%3(1 1 0)
%3function name? ∩f*\%1Ordinary multiplication, as above
%3choices?\%1the system already knows it.
%3 (0 1 1)
%3function name? imult-1
precondition? Integer(y) ∧ Integer(z).
postcondition? Integer(x).
body-name? idiv-1
choices?
(1 0 1)
function name? imult-2
precondition? Integer(x) ∧ Integer(z).
postcondition? Integer(y).
body-name? idiv-2
choices?
.
body-defs:
idiv-1?
imult(0 x 0)
imult(undef 0 x) ← ≠(x 0)
imult(x y z) ← ∩f//(z y x), imult(x y z).\%1This may look strange but it will
\be able to sort out which
\imult to use.
%3idiv-2:
imult(x 0 0)
imult(0 undef x) ← ≠(x 0)
imult(x y z) ← ∩f//(z x y), imult(x y z).
(PUTPROP 'IMULT '(((1 1 0) . ∩F*) ((0 1 1) . IMULT-1) ((1 0 1) . IMULT-2))
'GENERIC)
(DEFUN IMULT-1 FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'IMULT-1 L))
(BKTRKCOND L
'(((!X T) (TRY (INTEGER !X T) (≥ !X 0 T))))))
(T 'UNDEF)))
(DEFUN IMULT-2 FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'IMULT-2 L))
(BKTRKCOND L
'(((!X T) (TRY (INTEGER !X T) (≥ !X 0 T))))))
(T 'UNDEF)))
END_OF_GENERIC_SPEC
%1***the above definitions rely heavily on the arithmetic already defined in the target
language. The following definitions may be considered more typical.***
%3
.group
function gcd\gcd(x y z)%1 means that the greatest
%3input-pattern? (1 1 0)\%1common divisor of %3x%1 and %3y%1 is %3z%1.%3
parameter list? (x y z)
precondition? Nat(x true) ∧ Nat(y true).
postcondition? Nat(z true).
body? gcd(0 0 undef)
gcd(0 x x)
gcd(x 0 x)
gcd(x y z) ← ≥(x y), add(y w x), gcd(w y z)
gcd(x y z) ← ≥(y x), add(x w y), gcd(x w z).
.apart
(DEFUN GCD FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'GCD L))
(BKTRKCOND L
'(((0 0 UNDEF) (TRY))
((0 !X !X) (TRY))
((!X 0 !X) (TRY))
((!X !Y !Z)
(TRY (≥ !X !Y)
(ADD-2 !Y !W !X)
(GCD !W !Y !Z)))
((!X !Y !Z)
(TRY (≥ !Y !X)
(ADD-2 !X !W !Y)
(GCD !X !W !Z))))))
(T 'UNDEF)))
.turn on "↑"
generic factor\factor(w n p r)%1 means%3 w=n↑p*r
%3parameter list? (w n p r)\%1and%3 p%1 is maximal%3
choices?
(0 1 1 1)
function name? factor-1
precondition? Nat(n true) ∧ Nat(p true) ∧ Nat(r true).
postcondition? Nat(w true).
body-name? mult-out
choices?
(1 1 0 0)
function name? factor-34
precondition? Nat(w true) ∧ Nat(n true).
postcondition? Nat(p true) ∧ Nat(r true).
body-name? ss-factor
choices?
.
body-defs:
mult-out?
factor(r n 0 r) ← gcd(r n 1)
factor(w n p r) ← imult(n r x), ∩fsub1(p p1), factor(w n p1 x).
ss-factor?
factor(w n 0 w) ← <(w n)
factor(w n 0 w) ← gcd(w n 1)
factor(w n p r) ← ≥(w n), imult(v n w), factor(v n p1 r), add(p1 1 p).
.group
(PUTPROP 'FACTOR '(((0 1 1 1) . FACTOR-1) ((1 1 0 0) . FACTOR-34))
'GENERIC)
.apart
.group
(DEFUN FACTOR-1 FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'FACTOR-1 L))
(BKTRKCOND L
'(((0 0 UNDEF) (TRY))
((0 !X !X) (TRY))
((!X 0 !X) (TRY))
((!X !Y !Z)
(TRY (≥ !X !Y)
(ADD-2 !Y !W !X)
(GCD !W !Y !Z)))
((!X !Y !Z)
(TRY (≥ !Y !X)
(ADD-2 !X !W !Y)
(GCD !X !W !Z))))))
(T 'UNDEF)))
.apart
(DEFUN FACTOR-34 FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'FACTOR-34 L))
(BKTRKCOND L
'(((0 0 UNDEF) (TRY))
((0 !X !X) (TRY))
((!X 0 !X) (TRY))
((!X !Y !Z)
(TRY (≥ !X !Y)
(ADD-2 !Y !W !X)
(GCD !W !Y !Z)))
((!X !Y !Z)
(TRY (≥ !Y !X)
(ADD-2 !X !W !Y)
(GCD !X !W !Z))))))
(T 'UNDEF)))
END_OF_GENERIC_SPEC
generic E
parameter list? (x n y z)
choices?
(1 1 1 0)
function name? E-4
precondition? Nat(x true) ∧ Nat(n true) ∧ Nat(y true).
postcondition? Nat(z true).
body-name? ebod-4
choices?
(1 1 0 1)
function name? E-3
precondition? Nat(x true) ∧ Nat(n true) ∧ Nat(z true).
postcondition? Nat(y true).
body-name? ebod-3
choices?
(0 1 1 1)
function name? E-1
precondition? Nat(y true) ∧ Nat(n true) ∧ Nat(z true).
postcondition? Nat(x true).
body-name? ebod-1
choices?
.
body-defs:
ebod-4?
E(0 n y 0) ← ≠(y 0)
E(x n 0 1) ← ≠(x 0)
E(1 n y 1)
E(x n y z) ← factor(x n p r), imult(p y q), add(n 1 n1), E(r n1 y s), factor(z n q s).
ebod-3?
E(x n 0 1) ← ≠(x 0)
E(x n y z) ← factor(x n p r), add(n 1 n1), factor(z n q s), imult(p y q), E(r n1 y s).
ebod-1?
E(0 n y 0) ← ≠(y 0)
E(1 n y 1)
E(x n y z) ← factor(z n q s), imult(p y q), add(n 1 n1), E(r n1 y s), factor(x n p r).
(PUTPROP 'E '(((1 1 1 0) . E-4) ((1 1 0 1) . E-3) ((0 1 1 1) . E-1)) 'GENERIC)
.group
(DEFUN E-4 FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'E-4 L))
(BKTRKCOND L
'(((0 0 UNDEF) (TRY))
((0 !X !X) (TRY))
((!X 0 !X) (TRY))
((!X !Y !Z)
(TRY (≥ !X !Y)
(ADD-2 !Y !W !X)
(GCD !W !Y !Z)))
((!X !Y !Z)
(TRY (≥ !Y !X)
(ADD-2 !X !W !Y)
(GCD !X !W !Z))))))
(T 'UNDEF)))
.apart
.group
(DEFUN E-3 FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'E-3 L))
(BKTRKCOND L
'(((0 0 UNDEF) (TRY))
((0 !X !X) (TRY))
((!X 0 !X) (TRY))
((!X !Y !Z)
(TRY (≥ !X !Y)
(ADD-2 !Y !W !X)
(GCD !W !Y !Z)))
((!X !Y !Z)
(TRY (≥ !Y !X)
(ADD-2 !X !W !Y)
(GCD !X !W !Z))))))
(T 'UNDEF)))
.apart
(DEFUN E-1 FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'E-1 L))
(BKTRKCOND L
'(((0 0 UNDEF) (TRY))
((0 !X !X) (TRY))
((!X 0 !X) (TRY))
((!X !Y !Z)
(TRY (≥ !X !Y)
(ADD-2 !Y !W !X)
(GCD !W !Y !Z)))
((!X !Y !Z)
(TRY (≥ !Y !X)
(ADD-2 !X !W !Y)
(GCD !X !W !Z))))))
(T 'UNDEF)))
END_OF_GENERIC_SPEC
generic exp \exp(x y z) %1means %3 x↑y=z
%3parameter list? (x y z)
choices?
(1 1 0)
function name? exp-3
precondition? Nat(x) ∧ Nat(y).
postcondition? Nat(z).
body-name? expo
choices?
(1 0 1)
function name? exp-2
precondition? Nat(x) ∧ Nat(z).
postcondition? Nat(y).
body-name? expo
choices?
(0 1 1)
function name? exp-1
precondition? Nat(z) ∧ Nat(y).
postcondition? Nat(x).
body-name? expo
choices?
.
body-defs:
expo?
exp(x y z) ← E(x 2 y z).
(PUTPROP 'EXP '(((1 1 0) . EXP-3) ((1 0 1) . EXP-2) ((0 1 1) . EXP-1))
'GENERIC)
(DEFUN EXP-3 FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'EXP-3 L))
(BKTRKCOND L
'(((0 0 UNDEF) (TRY))
((0 !X !X) (TRY))
((!X 0 !X) (TRY))
((!X !Y !Z)
(TRY (≥ !X !Y)
(ADD-2 !Y !W !X)
(GCD !W !Y !Z)))
((!X !Y !Z)
(TRY (≥ !Y !X)
(ADD-2 !X !W !Y)
(GCD !X !W !Z))))))
(T 'UNDEF)))
.group
(DEFUN EXP-2 FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'EXP-2 L))
(BKTRKCOND L
'(((0 0 UNDEF) (TRY))
((0 !X !X) (TRY))
((!X 0 !X) (TRY))
((!X !Y !Z)
(TRY (≥ !X !Y)
(ADD-2 !Y !W !X)
(GCD !W !Y !Z)))
.apart
.group
((!X !Y !Z)
(TRY (≥ !Y !X)
(ADD-2 !X !W !Y)
(GCD !X !W !Z))))))
(T 'UNDEF)))
.apart
(DEFUN EXP-1 FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'EXP-1 L))
(BKTRKCOND L
'(((0 0 UNDEF) (TRY))
((0 !X !X) (TRY))
((!X 0 !X) (TRY))
((!X !Y !Z)
(TRY (≥ !X !Y)
(ADD-2 !Y !W !X)
(GCD !W !Y !Z)))
((!X !Y !Z)
(TRY (≥ !Y !X)
(ADD-2 !X !W !Y)
(GCD !X !W !Z))))))
(T 'UNDEF)))
END_OF_GENERIC_SPEC
type is-set
body?
is-set('mt-set,true)
is-set( add-elem(x,s), true) ← is-set(s, true), set-mem(x, s, false).
(DEFUN IS-SET FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'IS-SET L))
(BKTRKCOND L
'((('MT-SET T) (TRY))
(((ADD-ELEM !X !S) T)
(TRY (IS-SET !S T)
(SET-MEM !X !S FALSE))))))
(T 'UNDEF)))
function set-mem
input pattern? (1 1 0)
parameter list? (x y z)
precondition? is-set(y, true).
postcondition? boolean(z, true).
body?
set-mem(x, 'mt-set, false)
set-mem(x, add-elem(x, s), true)
set-mem(x, add-elem(y, s), true) ← set-mem(x, s, true)
set-mem(x, add-elem(y, s), false) ← same(x, y, z), same(z, false, true),
set-mem(x, s, false).
(DEFUN SET-MEM FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'SET-MEM L))
(BKTRKCOND L
'(((!X 'MT-SET FALSE) (TRY))
((!X (ADD-ELEM !X !S) T) (TRY))
((!X (ADD-ELEM !Y !S) T)
(TRY (SET-MEM !X !S T)))
((!X (ADD-ELEM !Y !S) FALSE)
(TRY (SAME !X !Y !Z)
(SAME !Z FALSE T)
(SET-MEM !X !S FALSE))))))
(T 'UNDEF)))
function same
input pattern? (1 1 0)
parameter list?
body?
same(x x true)
same(x y false).
(DEFUN SAME FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'SAME L))
(BKTRKCOND L
'(((!X !X T) (TRY)) ((!X !Y FALSE) (TRY)))))
(T 'UNDEF)))
function union
input pattern? (1 1 0)
parameter list? (x y z)
precondition? is-set(x, true) ∧ is-set(y,true).
postcondition? is-set(z, true).
body?
union('mt-set, y, y)
union(x, 'mt-set, x)
union(add-elem(x,s), y, add-elem(x,z)) ← set-mem(x, y, false), union(s, y, z)
union(add-elem(x,s), y, z) ← set-mem(x, y, true), union(s, y, z).
.group
(DEFUN UNION FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'UNION L))
(BKTRKCOND L
'((('MT-SET !Y !Y) (TRY))
((!X 'MT-SET !X) (TRY))
(((ADD-ELEM !X !S) !Y (ADD-ELEM !X !Z))
(TRY (SET-MEM !X !Y FALSE)
(UNION !S !Y !Z)))
(((ADD-ELEM !X !S) !Y !Z)
(TRY (SET-MEM !X !Y T)
(UNION !S !Y !Z))))))
(T 'UNDEF)))
.apart
type Intlist
body?
Intlist((),true)
Intlist(cons(x, l), true) ← Integer(x, true), Intlist(l, true).
(DEFUN INTLIST FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'INTLIST L))
(BKTRKCOND L
'(((NIL T) (TRY))
(((CONS !X !L) T)
(TRY (INTEGER !X T) (INTLIST !L T))))))
(T 'UNDEF)))
function Insertsort
input pattern? (1 0)
parameter list? (x y)
precond? Intlist(x, true).
postcond? Intlist(y, true) ∧ Perm(x, y, true).
body?
Insertsort((),())
Insertsort(cons(x,l), y) ← Insertsort(l, w), Insert(x, w, y).
(DEFUN INSERTSORT FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'INSERTSORT L))
(BKTRKCOND L
'(((NIL NIL) (TRY))
(((CONS !X !L) !Y)
(TRY (INSERTSORT !L !W)
(INSERT !X !W !Y))))))
(T 'UNDEF)))
function Insert
input pattern? (1 1 0)
parameter list? (x y z)
precond? Integer(x, true) ∧ Intlist(y, true).
postcond? Intlist(z, true).
body?
Insert(x, (), cons(x, ()))
Insert(x, cons(y,l), cons(x, cons(y,l))) ← ∩p≤(x, y, true)
Insert(x, cons(y,l), cons(y,z)) ← ∩p>(x, y, true), Insert(x, l, z).
(DEFUN INSERT FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'INSERT L))
(BKTRKCOND L
'(((!X NIL (CONS !X NIL)) (TRY))
((!X (CONS !Y !L) (CONS !X (CONS !Y !L)))
(TRY (∩P≤ !X !Y T)))
((!X (CONS !Y !L) (CONS !Y !Z))
(TRY (∩P> !X !Y T) (INSERT !X !L !Z))))))
(T 'UNDEF)))
function Selectionsort
input pattern? (1 0)
parameter list? (x y)
precond? Intlist(x, true).
postcond? Intlist(y, true) ∧ Perm(x, y, true).
body?
Selectionsort((), ())
Selectionsort(cons(x,u1), cons(y,u)) ← Partition-by-min(cons(x,u1), y, u2),
Selectionsort(u2, u).
(DEFUN SELECTIONSORT FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'SELECTIONSORT L))
(BKTRKCOND L
'(((NIL NIL) (TRY))
(((CONS !X !U1) (CONS !Y !U))
(TRY (PARTITION-BY-MIN (CONS !X !U1)
!Y
!U2)
(SELECTIONSORT !U2 !U))))))
(T 'UNDEF)))
function Partition-by-min
input pattern? (1 0 0)
parameter list? (u1 x u2)
precond? Intlist(u1, true) ∧ Non-empty(u1, true).
postcond? Integer(x, true) ∧ Intlist(u2, true).
body?
Partition-by-min(cons(x,()), x, ())
Partition-by-min(cons(x, cons(y,u)), z, cons(y,u1)) ←
∩p≤(x, y, true), Partition-by-min(cons(x,u), z, u1)
Partition-by-min(cons(x, cons(y,u)), z, cons(x,u1)) ←
∩p>(x, y, true), Partition-by-min(cons(y,u), z, u1).
(DEFUN PARTITION-BY-MIN FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'PARTITION-BY-MIN L))
(BKTRKCOND L
'((((CONS !X NIL) !X NIL) (TRY))
(((CONS !X (CONS !Y !U)) !Z (CONS !Y !U1))
(TRY (∩P≤ !X !Y T)
(PARTITION-BY-MIN (CONS !X !U)
!Z
!U1)))
(((CONS !X (CONS !Y !U)) !Z (CONS !X !U1))
(TRY (∩P> !X !Y T)
(PARTITION-BY-MIN (CONS !Y !U)
!Z
!U1))))))
(T 'UNDEF)))
function Non-empty
input pattern? (1 0)
parameter list? (l x)
precond? List(l, true).
postcond? Boolean(x, true).
body?
Non-empty((),false)
Non-empty(cons(y, u), true).
(DEFUN NON-EMPTY FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'NON-EMPTY L))
(BKTRKCOND L
'(((NIL FALSE) (TRY))
(((CONS !Y !U) T) (TRY)))))
(T 'UNDEF)))
.group
function Perm
input pattern? (1 0)
parameter list? (x y z)
precond? List(x, true) ∧ List(y, true).
postcond? Boolean(z, true).
body?
Perm( (), (), true)
Perm(cons(x,u1), cons(x,u2), true) ← Perm(u1, u2, true)
Perm(cons(x,u1), cons(y,u2), true) ← Delete(x, u2, u3),
Delete(y, u2, u4), Perm(u3, u4, true).
.apart
(DEFUN PERM FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'PERM L))
(BKTRKCOND L
'(((NIL NIL T) (TRY))
(((CONS !X !U1) (CONS !X !U2) T)
(TRY (PERM !U1 !U2 T)))
(((CONS !X !U1) (CONS !Y !U2) T)
(TRY (DELETE !X !U2 !U3)
(DELETE !Y !U2 !U4)
(PERM !U3 !U4 T))))))
(T 'UNDEF)))
function Delete
input pattern? (1 1 0)
parameter list? (x u1 u2)
precond? List(u1, true).
postcond? List(u2, true) ∧ Perm(cons(x, u2), u1, true).
body?
Delete(x, (), undef)
Delete(x, cons(x,l), l)
Delete(x, cons(y,l), undef) ← Delete(x, l, undef)
Delete(x, cons(y,u1), cons(y,u2)) ← Delete(x, u1, u2).
(DEFUN DELETE FEXPR (L)
(COND ((TRUE-PRECOND (CONS 'DELETE L))
(BKTRKCOND L
'(((!X NIL UNDEF) (TRY))
((!X (CONS !X !L) !L) (TRY))
((!X (CONS !Y !L) UNDEF)
(TRY (DELETE !X !L UNDEF)))
((!X (CONS !Y !U1) (CONS !Y !U2))
(TRY (DELETE !X !U1 !U2))))))
(T 'UNDEF)))
.group
function Fact
input pattern? (1 0)
parameter list? (x y)
precond? Integer(x, true) ∧ Greaterequal(x, 0, true).
postcond? Integer(y, true) ∧ Lessthan(0, y, true).
body? Fact(0 1)
Fact(x, y) ← Sub1(x, x1), Fact(x1, y1), Times(x, y1, y).
.apart
%1The above specification for the factorial function results in the following
Pascal program.
.begin turn off"↑"
PROGRAM G0002,FACT;
TYPE
ALLTYPS = (INTEGERTYP, REALTYP, BOOLEANTYP,
CHARTYP, SYMBOLTYP);
TERMTYPS = (VARIABLE, CONSTANTTYP, FUNAPP);
TERM = ↑T1;
TERMLIST = ↑TL1;
CONSTANT = ↑C1;
SYMBOL = ↑SYM1;
T1 = RECORD
CASE TTYP:TERMTYPS OF
VARIABLE: (VR: INTEGER);
CONSTANTTYP: (CNST: CONSTANT);
FUNAPP: (FNAME: SYMBOL;
ARGS: TERMLIST)
END;
TL1 = RECORD
NOTEMPTY: BOOLEAN;
FIRST: TERM;
REST: TERMLIST
END;
C1 = RECORD
CASE CTYP:ALLTYPS OF
INTEGERTYP: (IVAL: INTEGER);
REALTYP: (RVAL: REAL);
BOOLEANTYP: (BVAL: BOOLEAN);
CHARTYP: (CVAL: CHAR);
SYMBOLTYP: (SVAL: SYMBOL)
END;
SYM1 = RECORD
NOTEMPTY: BOOLEAN;
FIRSTCH: CHAR;
TAIL: SYMBOL;
END;
VARPAIRS = ↑VP;
VP = RECORD
NOTEMPTY: BOOLEAN;
OLD: INTEGER;
NEW: INTEGER;
REST: VARPAIRS
END;
FUNCTION GREATEREQUAL(X, Y: TERM; VAR Z: TERM): BOOLEAN;
EXTERN;
FUNCTION SUB1(X:TERM; VAR Y: TERM): BOOLEAN;
EXTERN;
FUNCTION TIMES(X, Y: TERM; VAR Z: TERM): BOOLEAN;
EXTERN;
FUNCTION OCCUR(X, Y: TERM): BOOLEAN;
EXTERN;
FUNCTION GENVAR: INTEGER;
EXTERN;
PROCEDURE REPLACE(X, T: TERM; VAR TML: TERMLIST);
EXTERN;
PROCEDURE SUBST(X, T: TERM; VAR T1, T2: TERMLIST);
EXTERN;
FUNCTION EQSYM(X, Y: SYMBOL): BOOLEAN;
EXTERN;
FUNCTION EQCONST(X, Y: CONSTANT): BOOLEAN;
EXTERN;
FUNCTION COPYSYM(OLDSYM: SYMBOL): SYMBOL;
EXTERN;
FUNCTION COPYTERM(OLDTM: TERM): TERM;
EXTERN;
FUNCTION COPYTERMLIST(TML: TERMLIST): TERMLIST;
EXTERN;
FUNCTION COPYCONST(OLDCONST: CONSTANT): CONSTANT;
EXTERN;
FUNCTION UNIFY(VAR X, Y, ALLX, ALLY: TERMLIST;
FAILED: BOOLEAN): BOOLEAN;
EXTERN;
PROCEDURE LOOKUP(TM: TERM; TBL: VARPAIRS;
FOUND: BOOLEAN);
EXTERN;
PROCEDURE STANDAPART(TML: TERMLIST;
VAR DONETBL: VARPAIRS);
EXTERN;
FUNCTION FACT(X : TERM ; VAR Y : TERM): BOOLEAN;
VAR
G0014, G0011, G0010, G0009, G0008, G0007, ACTUALS, COPYACTUALS
, MATCHLIST: TERMLIST;
G0015, G0012, Z1, W1, W, Z, G0005, G0003: TERM;
G0016, G0013, G0006, G0004: CONSTANT;
DONETBL: VARPAIRS;
FLAG, FAILED: BOOLEAN;
BEGIN
IF
(GREATEREQUAL (X, G0003, G0005))
THEN BEGIN
NEW(ACTUALS);
ACTUALS↑.NOTEMPTY := FALSE;
NEW(G0008);
G0008↑.NOTEMPTY := TRUE;
G0008↑.FIRST := Y;
G0008↑.REST := ACTUALS;
ACTUALS := G0008;
NEW(G0007);
G0007↑.NOTEMPTY := TRUE;
G0007↑.FIRST := X;
G0007↑.REST := ACTUALS;
ACTUALS := G0007;
COPYACTUALS := COPYTERMLIST(ACTUALS);
NEW(DONETBL);
DONETBL↑.NOTEMPTY := FALSE;
STANDAPART(COPYACTUALS, DONETBL);
NEW(MATCHLIST);
MATCHLIST↑.NOTEMPTY := FALSE;
NEW(G0014);
G0014↑.NOTEMPTY := TRUE;
NEW(G0015);
G0015↑.TTYP := CONSTANTTYP;
NEW(G0016);
G0016↑.CTYP := INTEGERTYP;
G0016↑.IVAL := 0;
G0015↑.CNST := G0016;
G0014↑.FIRST := G0015;
G0014↑.REST := MATCHLIST;
MATCHLIST := G0014;
NEW(G0011);
G0011↑.NOTEMPTY := TRUE;
NEW(G0012);
G0012↑.TTYP := CONSTANTTYP;
NEW(G0013);
G0013↑.CTYP := INTEGERTYP;
G0013↑.IVAL := 1;
G0012↑.CNST := G0013;
G0011↑.FIRST := G0012;
G0011↑.REST := MATCHLIST;
MATCHLIST := G0011;
IF UNIFY(COPYACTUALS , MATCHLIST,
COPYACTUALS, MATCHLIST, FAILED)
THEN BEGIN
FAILED := NOT TRUE
END
ELSE FAILED := TRUE;
COPYACTUALS := COPYTERMLIST(ACTUALS);
NEW(DONETBL);
DONETBL↑.NOTEMPTY := FALSE;
STANDAPART(COPYACTUALS, DONETBL);
NEW(MATCHLIST);
MATCHLIST↑.NOTEMPTY := FALSE;
NEW(G0010);
G0010↑.NOTEMPTY := TRUE;
NEW(W);
W↑.TTYP := VARIABLE;
W↑.VR := GENVAR;
G0010↑.FIRST := W;
G0010↑.REST := MATCHLIST;
MATCHLIST := G0010;
NEW(G0009);
G0009↑.NOTEMPTY := TRUE;
NEW(Z);
Z↑.TTYP := VARIABLE;
Z↑.VR := GENVAR;
G0009↑.FIRST := Z;
G0009↑.REST := MATCHLIST;
MATCHLIST := G0009;
IF UNIFY(COPYACTUALS , MATCHLIST,
COPYACTUALS, MATCHLIST, FAILED)
THEN BEGIN
NEW(W1);
W1↑.TTYP := VARIABLE;
W1↑.VR := GENVAR;
NEW(W1);
W1↑.TTYP := VARIABLE;
W1↑.VR := GENVAR;
NEW(Z1);
Z1↑.TTYP := VARIABLE;
Z1↑.VR := GENVAR;
NEW(Z1);
Z1↑.TTYP := VARIABLE;
Z1↑.VR := GENVAR;
FAILED := NOT (SUB1 (W W1) AND FACT (W1 Z1)
AND TIMES (W Z1 Z))
END
ELSE FAILED := TRUE;
FLAG := NOT FAILED;
FACT := FLAG;
IF FLAG
THEN BEGIN
X :=COPYACTUALS↑.FIRST;
COPYACTUALS := COPYACTUALS↑.REST;
Y :=COPYACTUALS↑.FIRST;
COPYACTUALS := COPYACTUALS↑.REST;
END
END
ELSE FACT := FALSE
END;
BEGIN END.
.end
.sec(Appendix B: Specification of a Program Synthesis System,,,P15:)
Note that %3env%1 is used to denote a global environment containing information
necessary to several of the following functions. The structure of %3env%1 is
a list of three elements: 1) a list of all generic function names along with their
selection lists; 2) a list of the names of all functions defined so far; and
3) a list of all types defined so far. The environment, %3env%1, is initialized
to a list consisting of three empty lists.
.begin nofill; select 3
function syn
input pattern? (1 1 1 0 0)
parameter list?
syn(speci, target, envinit, program, newenv) ←
firstsym(speci, nxtsym, spec),
int(nxtsym, spec, envinit, int-prog, newenv),
trans(int-prog, newenv, target, program).
function int
input pattern? (1 1 1 0 0)
parameter list?
int('function, spec, oldenv, int-prog, newenv) ←
fun-spec(spec, oldenv, int-prog, newenv)
int('type, spec, oldenv, int-prog, newenv) ←
type-spec(spec, oldenv, int-prog, newenv)
int('generic, spec, oldenv, int-prog, newenv) ←
gen-spec(spec, oldenv, int-prog, newenv).
function fun-spec
input pattern? (1 1 0 0)
parameter list?
fun-spec(spec, oldenv, list('function, name, inpat, params, precond, postcond, body),
newenv) ←
firstsym(spec, name, more2),
write("input-pattern?"), firstexp(more2, inpat, more3),
write("parameter list?"), firstexp(more3, params, more4),
write("precondition?"), is-disjunct(more4, precond, more5),
write("postcondition?"), is-disjunct(more5, postcond, more6),
addfun(oldenv, name, newenv),
write("body?"), is-body(more6, body, moren, undef, newenv, inpat).
function is-disjunct
input pattern? (1 0 0)
parameter list?
is-disjunct(spec, disj, more) ←
is-conjunct(spec, conj, more1, nxtsym),
finish-disj(more1, nxtsym, conj, disj, more).
function finish-disj
input pattern?(1 1 1 0 0)
parameter list?
finish-disj(spec, '∨, conj, list('∨, conj, disj), more) ←
is-disjunct(spec, disj, more)
finish-disj(spec, '/., conj, conj, spec).
function is-conjunct
input pattern? (1 0 0 0)
parameter list?
is-conjunct(spec, conj, more, nxtsym) ←
firstsym(spec, litsym, more1),
is-literal(litsym, more1, lit, more2, midsym),
finish-conj(more2, midsym, lit, conj, more, nxtsym).
function finish-conj
input pattern? (1 1 1 0 0 0)
parameter list?
finish-conj(spec, '∧, lit, list('∧, lit, conj), more, nxtsym) ←
is-conjunct(spec, conj, more, nxtsym)
finish-conj(spec, '/., lit, lit, spec, '/.).
function is-literal
input pattern? (1 1 0 0 0)
parameter list?
is-literal('TRUE, spec, T, more, nxtsym) ← firstsym(spec, nxtsym, more)
is-literal('T, spec, T, more, nxtsym) ← firstsym(spec, nxtsym, more)
is-literal('/(, spec, disj, more, nxtsym) ← is-disjunct(spec, disj, more1),
firstsym(more1, '/), more2), firstsym(more2, nxtsym, more)
is-literal(name, spec, atmf, more, nxtsym) ← firstsym(spec, '/(, more1),
is-funapp(name, more1, atmf, more, nxtsym).
function is-funapp
input pattern? (1 1 0 0 0)
parameter list?
is-funapp(name, spec, cons(name, arglist), more, nxtsym) ←
is-arglist(spec, arglist, more, nxtsym).
function is-arglist
input pattern? (1 0 0 0)
parameter list?
is-arglist(spec, arglist, more, nxtsym) ←
firstsym(spec, argsym, more2),
read-args(argsym, more2, arglist, more,nxtsym).
function read-args
input pattern? (1 1 0 0 0)
parameter list?
read-args('/), spec, (), more, nxtsym) ← firstsym(spec, nxtsym, more)
read-args(argsym, spec, cons(arg,arglist), more, nxtsym) ←
is-arg(argsym, spec, arg, more1, midsym),
read-args(midsym, more1, arglist, more, nxtsym).
function is-arg
input pattern? (1 1 0 0 0)
parameter list?
is-arg(argsym, spec, const, more, nxtsym) ← is-constnt(argsym, spec, const, more1),
firstsym(more1, nxtsym, more)
is-arg(name, spec, arg, more, lastsym) ← firstsym(spec, nxtsym, more1),
finish-arg(nxtsym, name, more1, arg, more, lastsym).
function finish-arg
input pattern? (1 1 1 0 0 0)
parameter list?
finish-arg('/(, name, spec, fnapp, more, nxtsym) ←
is-funapp(name, spec, fnapp, more, nxtsym)
finish-arg(nxtsym, name, spec, name, spec, nxtsym).
function is-constnt
input pattern? (1 1 0 0)
parameter list?
is-constnt('/', spec, list('quote,exp), more) ←
firstexp(spec, exp, more)
is-constnt(number, spec, number, more) ← integer(number)
is-constnt(number, spec, number, more) ← real(number)
is-constnt('undef, spec, undef, more)
is-constnt('false, spec, false, more)
is-constnt('true, spec, t, more)
is-constnt('t, spec, t, more)
is-constnt('/(, spec, (), more) ← firstsym(spec,'/),more).
function is-body
input pattern? (1 0 0 1 1 1)
parameter list?
is-body(spec,cons('bktrkcond,alternatives),more,genflag,env,inpat) ←
firstsym(spec, sym, more1),
is-hornclauses(sym, more1,alternatives,more,genflag,env,inpat).
function is-hornclauses
input pattern? (1 1 0 0 1 1 1)
parameter list?
is-hornclauses('/., spec,(),more,genflag,env,inpat)
is-hornclauses(name, spec, cons(match-try-pair,alternatives),
more,genflag,env,inpat) ←
firstsym(spec, '/(, spec2),
is-hclause(name,spec2,match-try-pair,more1,genflag,env,inpat,nxtsym),
is-hornclauses(nxtsym,more1,alternatives,more,genflag,env,inpat).
function is-hclause
input pattern? (1 1 0 0 1 1 1 0)
parameter list?
is-hclause(name,spec,list(arglist,trylist),more,genflag,env,inpat,lastsym) ←
is-funapp(name,spec,cons(name,arglist),more1,nxtsym),
finish-hclause(nxtsym, name, arglist, inpat, genflag, env, more1,
trylist, lastsym).
function finish-hclause
input pattern? (1 1 1 1 1 1 1 0 0 0)
parameter list?
finish-hclause('←, name, arglist, inpat, genflag, env, spec, trylist,
more, nxtsym) ←
mk-known(inpat, arglist, (), knownvars),
is-subgoalist(spec, trylist, more, env, knownvars, genflag, nxtsym)
finish-hclause(nxtsym, name, arglist, inpat, genflag, env, spec,
cons('try, ()), spec, nxtsym).
function is-subgoalist
input pattern? (1 0 0 1 1 1 0)
parameter list?
is-subgoalist(spec,cons('try,cons(cons(fname,arglist),sbglist)),more,env,
knownvars,false,lastsym) ←
firstsym(spec,name,spec2), firstsym(spec2, '/(, spec3),
is-funapp(name,spec3,cons(name,arglist),more1,nxtsym),
ck-generic(name,env,arglist, knownvars,fname),
mk-allknown(arglist,knownvars,newknownvars),
rd-subgoals(nxtsym,more1,sbglist,more,env,newknownvars,false,lastsym)
is-subgoalist(spec,cons('try,cons(cons(name,arglist),sbglist)),more,env,
knownvars,true,lastsym) ←
firstsym(spec,name,spec2), firstsym(spec2, '/(, spec3),
is-funapp(name, spec3,cons(name,arglist),more1,nxtsym),
rd-subgoals(nxtsym,more1,sbglist,more,env,knownvars,true,lastsym).
function rd-subgoals
input pattern? (1 1 0 0 1 1 1 0)
parameter list?
rd-subgoals('/,,spec,cons(cons(name,arglist),sbglist),
more,env,knownvars,true,lastsym) ←
firstsym(spec,name,more1), firstsym( more1, '/(, more12),
is-funapp(name,more12,cons(name,arglist),more2,nxtsym),
rd-subgoals(nxtsym,more2,sbglist,more,env,knownvars,true,lastsym)
rd-subgoals('/,,spec,cons(cons(fname,arglist),sbglist),
more,env,knownvars,false,lastsym) ←
firstsym(spec,name,more1), firstsym(more1, '/(, more21),
is-funapp(name,more21,cons(name,arglist),more2,nxtsym),
ck-generic(name,env,arglist,knownvars,fname),
mk-allknown(arglist,knownvars,newknownvars),
rd-subgoals(nxtsym,more2,sbglist,more,env,newknownvars,false,lastsym)
rd-subgoals(nxtsym, spec, (), spec, env, knownvars, genflag, nxtsym) .
function ck-generic
input pattern? (1 1 1 1 0)
parameter list?
ck-generic(name, env, arglist, knownvars, name) ← generic(name, env, undef)
ck-generic(name, env, arglist, knownvars, fname) ←
generic(name, env, selections),
mk_pat(arglist, knownvars, inpat),
choose-fun(inpat, selections, fname).
function generic
input pattern? (1 1 0)
parameter list?
generic(name,list(generics,functions, types), selections) ←
findin(name,generics,selections).
function findin
input pattern? (1 1 0)
parameter list?
findin(name, (), 'undef)
findin(name, cons(cons(name,x),y), x)
findin(name, cons(cons(other,x),y), z) ← findin(name,y,z).
function addfun
input pattern? (1 1 0)
parameter list?
addfun(list(generics,functions,types),name,
list(generics, cons(name,functions),types)).
function not-in
input pattern? (1 1)
parameter list?
not-in(x,())
not-in(x,l) ← member(x,l,false).
function member
input pattern? (1 1 0)
parameter list?
member(x,cons(x,l),true)
member(x,cons(y,l),ans) ← member(x,l,ans)
member(x,(),false).
function mk-allknown
input pattern? (1 1 0)
parameter list?
mk-allknown((),knownvars,knownvars)
mk-allknown(cons(x,l), knownvars, newknownvars) ← vars_in(x,vl),
mk-allknown(l, knownvars, nkv), append$(vl, nkv, newknownvars).
function mk-known
input pattern? (1 1 1 0)
parameter list?
mk-known((), (), knownvars, knownvars)
mk-known(cons(1,l), cons(x,k), knownvars, newknownvars) ← vars_in(x,vl),
mk-known(l,k,knownvars, nkv), append$(vl, nkv, newknownvars)
mk-known(cons(0,l), cons(x,k), knownvars, newknownvars) ←
mk-known(l, k, knownvars, newknownvars).
function vars_in
input pattern? (1 0)
parameter list?
vars_in(exp,()) ← itsaconstant(exp,true)
vars_in(exp, cons(exp,())) ← itsavar(exp,true)
vars_in(cons(name,arglist), varlist) ← varsinlist(arglist, varlist).
function varsinlist
input pattern? (1 0)
parameter list?
varsinlist((), ())
varsinlist(cons(s,l), varlist) ← vars_in(x, varlist1),
varsinlist(l, varlist2), append$(varlist1, varlist2, varlist).
function itsaconstant
input pattern? (1 0)
parameter list?
itsaconstant(x, true) ← itsanumber(x, true)
itsaconstant(cons('quote,l), true)
itsaconstant(t, true)
itsaconstant('undef, true)
itsaconstant((), true)
itsaconstant('false, true)
itsaconstant('true, true)
itsaconstant('f, true)
itsaconstant(x, true) ← is-string(x).
function itsanumber
input pattern? (1 0)
parameter list?
itsanumber(x,true) ← real(x)
itsanumber(x, true) ← integer(x).
function itsavar
input pattern? (1 0)
parameter list?
itsavar(cons(x,y), false)
itsvar(exp, true) ← itsaconstant(exp, false).
function append$
input pattern? (1 1 0)
parameter list?
append$(x,(),x)
append$( (), x, x)
append$(cons(x,l1), l2, cons(x,l3)) ← append$(l1, l2, l3).
function choose-fun
input pattern? (1 1 0)
parameter list?
choose-fun(inpat, cons(pattern, cons(fname, sels)), fname) ←
enuf-known(inpat, pattern, true)
choose-fun(inpat, cons(pattern, cons(fname,sels)), funname) ←
choose-fun(inpat, sels, funname)
choose-fun(inpat, (), undef).
function enuf-known
input pattern? (1 1 0)
parameter list?
enuf-known((), (), true)
enuf-known(cons(1,l), cons(x,k), ans) ← enuf-known(l,k,ans)
enuf-known(cons(0,l), cons(1,k), false).
function mk_pat
input pattern? (1 1 0)
parameter list?
mk_pat( (), knownvars, ())
mk_pat(cons(arg,l), knownvars, cons(1,k)) ←
is-known(arg, knownvars, true), mk_pat(l, knownvars, k)
mk_pat(cons(arg,l), knownvars, cons(0,k)) ← mk_pat(l, knownvars, k).
function is-known
input pattern? (1 1 0)
parameter list?
is-known(x, knownvars, true) ← itsaconstant(x,true)
is-known(cons(f,l), knownvars,ans) ← known-list(l, knownvars, ans)
is-known(x, knownvars, ans) ← member(x, knownvars, ans).
function knownlist
input pattern? (1 1 0)
parameter list?
known-list((), knownvars, true)
known-list(cons(x,l), knownvars, true) ← is-known(x, knownvars, true),
known-list(l,knownvars,true).
function type-spec
input pattern? (1 1 0 0)
parameter list?
type-spec(spec,oldenv,
list('type,name,'(1 0), '(x y), T, '(boolean y),body), newenv) ←
firstsym(spec, name, more1),
add-type(oldenv, name, newenv),
write("body?"),
is-body(more1, body, morex, undef, newenv, '(1 0)).
function add-type
input pattern? (1 1 0)
parameter list?
add-type(list(generics,functions,types), name,
list(generics,functions, cons(name,types))).
function gen-spec
input pattern? (1 1 0 0)
parameter list?
gen-spec(spec, oldenv,
cons(list('generic, name, params, selections), deflist), newenv) ←
firstsym(spec, name, more1),
write("parameter list?"), firstexp(more1, params, more2),
write("choices?"), firstsym(more2, nxtsym, more3),
rd-choices(nxtsym, more3, choicelist, bodylist, more4),
add-gen(oldenv, name, choicelist, newenv),
repeats-of(bodylist, rep-bodnams),
write("body-defs:"),
rd-bodies(more4, choicelist, (), (), params, rep-bodnams, newenv,
deflist, morex).
function rd-choices
input pattern? (1 1 0 0 0)
parameter list?
rd-choices('/., spec, (), (), more)
rd-choices('/(, spec, cons(list(inpat,name,precond,postcond,bodnam), choicelist),
cons(bodnam,bodylist), more) ←
firstsym(spec, nxtsym, spec2),
readinpat(nxtsym, spec2, inpat, more1), write("function name?"),
firstsym(more1, name, more2), write("precondition?"),
is-disjunct(more2, precond, more3),
write("postcondition?"),
is-disjunct(more3, postcond, more4),
write("body name?"),
firstsym(more4, bodnam, more5),
write("choices?"), firstsym(more5, chsym, more6),
rd-choices(chsym, more6, choicelist, bodylist, more).
function readinpat
input pattern? (1 1 0 0)
parameter list?
readinpat('/), spec, (), spec)
readinpat(digit, spec, cons(digit, restinpat), more) ←
firstsym(spec, nxtsym, more1),
readinpat(nxtsym, more1, restinpat, more).
function rd-bodies
input pattern? (1 1 1 1 1 1 1 0 0)
parameter list?
rd-bodies(spec, (), rep-bodies, donelist, params, rep-bodnams, env, (), spec)
rd-bodies(spec, cons(list(inpat,name,precond,postcond,bodnam), choicelist),
rep-bodies, donelist, params, rep-bodnams,env,
cons(list('function,name,inpat,params,precond,postcond,body), deflist),
more) ←
not-in(bodnam, donelist), not-in(bodnam,rep-bodnams),
write(bodnam), write("?"),
is-body(spec, body, more1, false, env, inpat),
rd-bodies(more1, choicelist, rep-bodies, cons(bodnam,donelist), params,
rep-bodnams, env, deflist, more)
rd-bodies(spec, cons(list(inpat,name,precond,postcond,bodnam), choicelist),
rep-bodies, donelist, params, rep-bodnams,env,
cons(list('function,name,inpat,params,precond,postcond,body), deflist),
more) ←
member(bodnam,donelist,true),
getb(bodnam, rep-bodies, genbody),
spec-body(inpat, env, genbody, body)
rd-bodies(spec, cons(list(inpat,name,precond,postcond,bodnam), choicelist),
cons(cons(bodnam,genbody),rep-bodies), donelist, params,
rep-bodnams,env,
cons(list('function,name,inpat,params,precond,postcond,body), deflist),
more) ←
not-in(bodnam, donelist), member(bodnam, rep-bodnams, true),
write(bodnam), write("?"),
is-body(spec, genbody, more1, true, env, inpat),
spec-body(inpat, env, genbody, body).
function getb
input pattern? (1 1 0)
parameter list?
getb(bodnam, cons(cons(bodnam,genbody), rep-bodies), genbody)
getb(bodnam, cons(x,repbodies), genbody) ←
getb(bodnam, repbodies, genbody).
function spec-body
input pattern? (1 1 1 0)
parameter list?
spec-body(inpat, env, cons('bktrkcond, genalternatives),
cons('bktrkcond, alternatives) ) ←
spec-alts(inpat, env, genalternatives, alternatives).
function spec-alts
input pattern? (1 1 1 0)
parameter list?
spec-alts(inpat, env, (), ())
spec-alts(inpat, env, cons(genmatch-try-pair, genalternatives),
cons(match-try-pair, alternatives)) ←
spec-clause(inpat, env, genmatch-try-pair, match-try-pair),
spec-alts(inpat, env, genalternatives, alternatives).
function spec-clause
input pattern? (1 1 1 0)
parameter list?
spec-clause(inpat, env, list(arglist, cons('try,genlist)),
list(arglist, cons('try,sblist))) ←
mk-known(inpat, arglist, (), knownvars),
spec-goalist(genlist, env, knownvars, sblist).
function spec-goalist
input pattern? (1 1 1 0)
parameter list?
spec-goalist((), env, knownvars, ())
spec-goalist(cons( cons(name,l), genlist), env, knownvars,
cons( cons(name,l),sblist)) ←
generic(name, env, undef),
mk-allknown(l, knownvars, newknownvars),
spec-goalist(genlist, env, newknownvars, sblist)
spec-goalist(cons(cons(genname,arglist), genlist), env, knownvars,
cons(cons(name,arglist), sblist)) ←
generic(genname, env, selections),
mk_pat(arglist, knownvars, inpat),
choose-fun(inpat, selections, name),
mk-allknown(arglist,knownvars, newknownvars),
spec-goalist(genlist, env, newkownvars, sblist).
function trans
input pattern? (1 1 1 0)
parameter list?
trans(list( 'function, name, inpat, params, precond, postcond,
cons('bktrkcond, alternatives)), env, 'lisp,
list( 'defun, name, 'fexpr, '(l),
list( 'cond list( list('trueprecond,list('cons,
list('quote, name)
'l)),
list('bktrkcond, 'l, list('quote,
alternatives))),
'(t 'undef))) ).
.end
.sec(Appendix C: Listing of the System)
The following listing is the actual program that is read into MACLSP.
The semi-colon indicates that everything until the next carriage-return is to
be taken as a comment.
.begin nofill
;top level
(def top ()
(prog (you-want-to-save)
; the next two lines should eventually be deleted, they make LISP the default language
(setq target 'lisp)
(makedefs (get 'lisp 'primdefs))
(setq namelist ())
(setq inflag t)
(setq prim-types '(integer real boolean is-string is-list))
(princ '|Hello, this is a program synthesis system which takes logic/
specifications as input and generates a program in the target/
language of your choice./
(Right now that choice is limited to LISP and maybe PASCAL). /
/
If you wish the output to go to a file, please give me the name/
of that file; if not, just hit carriage-return/
|)
(readch)(readch)
((lambda (filename)
(cond ((eq filename carriage_return) (setq outflag nil))
(t (setq outputfile (read))
(uwrite dsk (j red))
(setq outflag t)
(setq ↑r t))))
(tyipeek))
(princ '|/
If you wish me to read specifications from a file you've created,/
then please give me the name of the file; if this session is to be/
interactive, then just hit carriage-return/
|)
(readch)(readch)
((lambda (filename)
(cond ((eq filename carriage_return) (setq inflag nil) (princ '|/
If you need help getting started, type "?"./
/
|))
(t (setq filename (read))
(setq inflag t)
(eval (list 'eread filename))
(setq ↑q t))))
(tyipeek))
(setq nxtsym (ratom))
(do () ((not (is_definition)) (print 'alldone))
(setq namelist (cons name namelist))
(putprop name params 'params)
(putprop name precond 'precond)
(putprop name inpat 'inpat)
(putprop name postcond 'postcond)
(putprop name body 'body)
((lambda (x) (cond ((eq target 'lisp)
(eval x) (eval (list 'grindef name)))
(t (unlist x))))
(translate name target))
(terpri)
(terpri)
(setq nxtsym (ratom)))
(cond (outflag
(eval (list 'ufile outputfile 'gen))))
(princ '|/
Do you want to save these internalized specifications on a file?/
If not, just hit carriage return... |)
(readch)
(readch)
(setq nxtsym (tyipeek))
(cond ((not (or (eq nxtsym carriage_return) (eq nxtsym $n)))
(setq you-want-to-save t) (setq nxtsym (read)))) ;you-want-to-save
(cond (you-want-to-save (princ '|/
on what file?/ |) ;is initialized to
;nil as prog var
((lambda (nam)
(dumpdefs namelist nam)
(princ '|/
Whenever you want to start the system up with these/
functions already defined as they were in this session,/
type/
"(include |)
(princ nam)(princ '|)"/
then type/
"(top)"/
Actually the call on include can take any number of/
filenames that you wish to include.|))
(read)))
(t (princ '|/
nothing saved/
|)))
(princ '|/
We now turn control back over to the top level of LISP. /
If you wish to start over type "(top)"/
|)))
(def is_definition ()
(do ()((not (eq nxtsym '?)))
(princ '|/
To specify the target language type:/
"target <language-name>"/
/
To specify a function definition type:/
"function <name>"/
followed by the rest of the specification. You will be asked for each/
part of the specification; if you don't know how to answer,/
type "?" for help./
/
To specify a generic function definition type:/
"generic <name>"/
followed by the rest of the specification. You will be asked for each/
part of the specification; if you don't know how to answer,/
type "?" for help./
/
To specify a data type type:/
"type <name>"/
followed by the rest of the specification. You will be asked for each/
part of the specification; if you don't know how to answer,/
type "?" for help./
/
To conclude the session type a period "."/
|)
(terpri)
(setq nxtsym (ratom)))
(setq genrlflag nil)
(cond ((is_fundef) (setq name fname)(putprop fname t 'function))
((is-gendef)(setq nxtsym (ratom)) (is_definition))
((is-typedef) (setq name typename)(putprop name t 'type))
((eq nxtsym 'target)(newtarget)(setq nxtsym (ratom))(is_definition))
((eq nxtsym '/.) nil)
(t (error '(bad start (or finish)) nxtsym))))
(def newtarget ()
(setq target (ratom))
(cond ((eq target 'lisp)
(setq deflist (get target 'primdefs))
(makedefs deflist))))
(def makedefs (dl) (cond ((null dl) t)
(t (eval (first dl)) (makedefs (rest dl)))))
(def dumpdefs (namelist filename)
(uwrite)
(setq ↑r t)
(setq ↑w t)
(do ((names namelist (rest names)))
((null names))
(prog (name)
(setq name (first names))
(print (list 'putprop (list 'quote name)
(list 'quote (get name 'params))
''params))
(print (list 'putprop (list 'quote name)
(list 'quote (get name 'precond))
''precond))
(print (list 'putprop (list 'quote name)
(list 'quote (get name 'postcond))
''postcond))
(print (list 'putprop (list 'quote name)
(list 'quote (get name 'inpat))
''inpat))
(print (list 'putprop (list 'quote name)
(list 'quote (get name 'body))
''body))
(print (list 'putprop (list 'quote name)
(list 'quote (get name 'fexpr))
''fexpr))
)) ;end of prog and do
(print ''*eof*)
(eval (list 'ufile filename 'ext))
(setq ↑w nil))
(def include fexpr (flnames)
(cond ((null flnames) 'all-done)
(t (eval (list 'eread (first flnames) 'ext))
(setq ↑q t)
(do ((x nil (eval (read))))
((eq x '*eof*)))
(eval (cons 'include (rest flnames))))))
(def unlist (l) (do ((dumplist l (rest dumplist))) ;this is for printing out
((null dumplist)) ;programs that were generated
(princ (first dumplist))))
.next page
;stuff needed all over
(putprop 'def (get 'defun 'fsubr) 'fsubr)
(setq $n 156)
(setq rpg-bug 315)
(setq ? 77)
(setq tab 11)
(setq period 56)
(setq dollar-sign 44)
(setq hot-cross-bun 26)
(setq comma 54)
(setq back-arrow 137)
(setq or-sym 37)
(setq and-sym 4)
(setq lpar 50)
(setq rpar 51)
(setq space 40)
(setq carriage_return 15)
(setq line_feed 12)
(def is_funapp ()
(prog (fname arglist) (return
(cond ((eq (typep nxtsym) 'symbol) (setq fname nxtsym)
(cond ((eq (setq nxtsym (ratom)) '/( )
(setq nxtsym (ratom))
(setq arglist (formalize
(readargs)))
(make_funapp fname arglist))
(t (error '(missing arglist) nxtsym))))
(t (error '(funapp with bad function name) nxtsym))))))
;no infix function applications are allowed in this version
(def readargs ()
(prog (arg)
(cond ((eq nxtsym '/,) (setq nxtsym (ratom))))
(return (cond ((eq nxtsym '/) ) (setq nxtsym (ratom)) ())
((eq (tyipeek) lpar) (cons (is_funapp) (readargs)))
((eq nxtsym '/() (cond ((eq (setq nxtsym (ratom)) '/))
(setq arg ())
(setq nxtsym (ratom))
(cons arg (readargs)))
(t (error '(unquoted non-empty list as arg)nxtsym))))
((atom nxtsym) (setq arg nxtsym) (setq nxtsym (ratom))
(cons arg (readargs)))
((eq (first nxtsym) 'quote) (setq arg nxtsym) (setq nxtsym (ratom))
(cons arg (readargs)))
((eq (first nxtsym) 'string) (setq arg nxtsym) (setq nxtsym (ratom))
(cons arg (readargs)))
(t (error '(weird argument) nxtsym))))))
(def make_funapp (x y) (cons x y))
(def ratom () (setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym tab) (eq nxtsym carriage_return))))
(setq nxtsym (readch))
(setq nxtsym (tyipeek)))
(cond ((or (eq nxtsym comma) (eq nxtsym back-arrow) (eq nxtsym period)
(eq nxtsym or-sym) (eq nxtsym and-sym)
(eq nxtsym lpar) (eq nxtsym rpar)) (setq nxtsym (readch)))
(t (setq nxtsym (read))
(cond ((eq nxtsym 'true) t)
((eq nxtsym 'f) 'false)
(t nxtsym)))))
(def first (x) (car x))
(def second (x) (cadr x))
(def third (x) (caddr x))
(def rest (x) (cdr x))
.next page
;The following programs accomplish the interactive input of function, type,
;and generic definitions. They are much longer than need be due to the
;voluminous help information.
(def is_fundef ()
(cond ( (eq nxtsym 'function)
(setq fname (read))
(princ '|/
input pattern? |)
(setq nxtsym (tyipeek))
(do () ((not (eq nxtsym ?)))
(setq nxtsym (readch))
(princ '|/
/
The input pattern is a list of 1's and 0's (optionally separated /
by commas) indicating which of the parameters are to be considered/
input (values available on procedure call) and which are output/
(values to be computed)/, respectively. For example/,/
"(1/, 1/, 0)"/
indicates that the last parameter is thought of as a function/
of the first two parameters./
/
input pattern? |)
(setq nxtsym (tyipeek)))
(setq inpat (read))
(princ '|/
parameter list?/ |)
(readch)(readch)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) )))
(setq nxtsym (readch)) (setq nxtsym (tyipeek)))
(do ()((not (eq nxtsym ?)))(setq nxtsym (readch))
(princ '|/
the parameter list is a list of variables, enclosed in parentheses,/
and optionally separated by commas. /
For example, "(x1, x2, x3)" |)
(terpri)(princ '|/
parameter list?/ |)
(cond ((not inflag) (readch)(readch)))
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) )))
(setq nxtsym (readch)) (setq nxtsym (tyipeek))))
(cond ((eq nxtsym carriage_return)
(setq params (make-up-args inpat))
(setq precond t)
(setq postcond t)
(princ '|/
you've just defaulted on formal parameters, precondition,/
and postcondition, you know that really is not a good idea./
/
body? |))
((eq nxtsym lpar)
(setq params (formalize (read)))
(princ '|/
precond?/ |)
(setq nxtsym (ratom))
(do ()((not (eq nxtsym '?)))
(princ '|/
a precondition is a disjunction, which expresses a condition /
or domain over which the function being defined is guaranteed/
to terminate. The disjunction must be terminated by a period.|) (terpri)
(princ '| /
domain-spec ::= disjunction "."/
/
disjunction ::= conjunction /| disjunction "∨" conjunction /
/
conjunction ::= literal /| conjunction "∧" literal /
/
literal ::= atomic-formula /| "¬" atomic-formula /
/
atomic-formula ::= "true" /| fun-app /| "(" disjunction ")" /
/
fun-app ::= name arglist /
/
arglist ::= "( )" /| "(" args ")"/
/
args ::= arg /| arg "," args /
/
arg ::= identifier /| number /| fun-app /
/
For example, "integer(x1,y) ∧ grtr-eq(x1,0,z)" /
Don't forget to include the output variables, in this case y and z.
|)
(terpri)(terpri)(princ '|precond? |)
(setq nxtsym (ratom)))
(setq precond (readspec))
(princ '|/
postcond?/ |)
(setq nxtsym (ratom))
(do ()((not (eq nxtsym '?)))
(princ '|/
A postcondition is a disjunction, which expresses a condition /
guaranteed to be true of the output variables. It might also/
be considered as a specification of the range of the function.|)
(princ '| /
range-spec ::= disjunction "."/
/
disjunction ::= conjunction /| disjunction "∨" conjunction /
/
conjunction ::= literal /| conjunction "∧" literal /
/
literal ::= atomic-formula /| "¬" atomic-formula /
/
atomic-formula ::= "true" /| fun-app /| "(" disjunction ")" /
/
fun-app ::= name arglist /
/
arglist ::= "( )" /| "(" args ")"/
/
args ::= arg /| arg "," args /
/
arg ::= identifier /| number /| fun-app /
/
For example, "integer(y,z) ∧ grtr(y,0,z)" /
(remember the output variables!)/
|)
(terpri)(princ '|/
postcond?/ |)
(setq nxtsym (ratom)))
(setq postcond (readspec))
(princ '|/
body?/ |))
(t (error '(no "/(" seen when asking for parameters) nxtsym)))
(setq nxtsym (ratom))
(do ()((not (eq nxtsym '?)))
(princ '|/
A function body is a set of horn clauses, terminated by a period./
/
body ::= horn-clauses "."/
/
horn-clauses ::= h-clause /| h-clause horn-clauses/
/
h-clause ::= goal "←" subgoals /| goal/
/
goal ::= fun-app/
/
subgoals ::= fun-app /| fun-app "," subgoals/
/
fun-app ::= name arglist /
/
For example:/
/
fact(0,1)/
fact(n,z) ← sub1(n,x), fact(x,z1), times(n,z1,z)/
|)
(terpri)(princ '|/
body?/ |)
(setq nxtsym (ratom)))
(setq body (repclauses)))
(t nil)))
(def make-up-args (list)
(cond ((null list) ())
(t (cons (gensym) (make-up-args (rest list))))))
(def is-gendef ()
(prog (specs gname params bodies-pair)
(return
(cond ( (eq nxtsym 'generic)
(setq gname (read))
(princ '|/
parameter list?/ |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek)))
(do ()((not (eq nxtsym ?)))(setq nxtsym (readch))
(princ '|/
the parameter list is a list of variables, enclosed in parentheses,/
and optionally separated by commas. /
For example, "(x1, x2, x3)" |)
(terpri)(princ '|/
parameter list?/ |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek))))
(setq params (formalize (read)))
(princ '|/
choices? |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek)))
(do ()((not (eq nxtsym ?)))(setq nxtsym (readch))
(princ '|/
a choice consists of an input pattern, function-name, precondition, postcondition,
and body-name. Just give the input pattern and the system will ask you for the
rest./
/
/
if there are no more choices to be entered type "."/
/
choices? |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek))))
(prog (fun-name inpat precond postcond body-name)
(setq specs
(do ( (selections () (cons (cons inpat fun-name) selections))
(flag () ()) ;flag tells whether fun-name is new
(bodies () (cond (flag (cons body-name bodies))
(t bodies)))
(fun-names () (cond (flag
(cons fun-name fun-names))
(t fun-names))) )
( (eq nxtsym period)
(setq nxtsym (ratom))
(cons selections (cons bodies fun-names)) )
(setq inpat (read))
(princ '|/
function name? |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek)))
(do ()((not (eq nxtsym ?)))(setq nxtsym (readch))
(princ '|/
this is the name the system will use to define a function with the given input
pattern, to be called whenever a generic call is made which fits the input-
pattern/
/
function name? |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek))))
(setq fun-name (read))
(cond
((get fun-name 'body) nil);if it is already defined, do nothing
((eq '%3∩%1 (first (explode fun-name)))
(autopred fun-name params)); if system function, autopred it
(t ;otherwise, get the rest of the info
(setq flag t)
(putprop fun-name inpat 'inpat)
(putprop fun-name params 'params)
(princ '|/
precond?/ |)
(setq nxtsym (ratom))
(cond ((eq nxtsym 'precond?) (setq nxtsym (ratom))))
(do ()((not (eq nxtsym '?)))
(princ '|/
a precondition is a disjunction, which expresses a condition /
or domain over which the function being defined is guaranteed/
to terminate. The disjunction must be terminated by a period.|) (terpri)
(princ '| /
domain-spec ::= disjunction "."/
/
disjunction ::= conjunction /| disjunction "∨" conjunction /
/
conjunction ::= literal /| conjunction "∧" literal /
/
literal ::= atomic-formula /| "¬" atomic-formula /
/
atomic-formula ::= "true" /| fun-app /| "(" disjunction ")" /
/
fun-app ::= name arglist /
/
arglist ::= "( )" /| "(" args ")"/
/
args ::= arg /| arg "," args /
/
arg ::= identifier /| number /| fun-app /
/
For example, "integer(x1,y) ∧ grtr-eq(x1,0,z)" /
Don't forget to include the output variables, in this case y and z.
|)
(terpri)(terpri)(princ 'precond? )
(setq nxtsym (ratom))
(cond ((eq nxtsym 'precond?) (setq nxtsym
(ratom)))))
(setq precond (readspec)) (putprop fun-name precond 'precond)
(princ '|/
postcond?/ |)
(setq nxtsym (ratom))
(cond ((eq nxtsym 'postcond?) (setq nxtsym (ratom))))
(do ()((not (eq nxtsym '?)))
(princ '|/
A postcondition is a disjunction, which expresses a condition /
guaranteed to be true of the output variables. It might also/
be considered as a specification of the range of the function.|)
(princ '| /
range-spec ::= disjunction "."/
/
disjunction ::= conjunction /| disjunction "∨" conjunction /
/
conjunction ::= literal /| conjunction "∧" literal /
/
literal ::= atomic-formula /| "¬" atomic-formula /
/
atomic-formula ::= "true" /| fun-app /| "(" disjunction ")" /
/
fun-app ::= name arglist /
/
arglist ::= "( )" /| "(" args ")"/
/
args ::= arg /| arg "," args /
/
arg ::= identifier /| number /| fun-app /
/
For example, "integer(y,z) ∧ grtr(y,0,z)" /
(remember the output variables!)/
|)
(terpri)(princ '|/
postcond?/ |)
(setq nxtsym (ratom))
(cond ((eq nxtsym 'postcond?)
(setq nxtsym (ratom)))))
(setq postcond (readspec)) (putprop fun-name postcond 'postcond)
(princ '|/
body-name? |)
(cond ((not inflag) (ratom)))
(setq nxtsym (ratom))
(do ()((not (eq nxtsym '?)))
(princ '|/
this is the name which associates the proper body definition with the function
being defined/
/
body-name?/ |)
(cond ((not inflag) (ratom)))
(setq nxtsym (ratom)))
(setq body-name nxtsym)
(putprop fun-name body-name 'bodyname)
));end of cond for defining fun-name
(princ '|/
choices? |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek)))
(do ()((not (eq nxtsym ?)))(setq nxtsym (readch))
(princ '|/
a choice consists of an input pattern, function-name, precondition, postcondition,
and body-name. Just give the input pattern and the system will ask you for the
rest./
/
if there are no more choices to be entered type "."/
/
choices? |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek))))
)))
;end of the "do" that gets all the choices and the setq of the result of "do"
;and the prog surrounding it
(print (make-gendef gname (reverse (first specs))))
(cond ((first (rest specs))
(setq bodies-pair (splitbodies (second specs) '(()()) ))
(setq namelist (append (rest (rest specs)) namelist))
(princ '|/
body-defs:|)
(prog (bodnam fun-name genrlflag genrldef)
(do ( (rep-bodies (second bodies-pair) rep-bodies)
(donebods () (cons bodnam donebods))
(fun-names (reverse (rest (rest specs))) (rest fun-names))
(rep-defs () (cond ((and genrlflag (not (member
bodnam donebods)))
(cons (cons bodnam genrldef) rep-defs))
(t rep-defs))) )
((null fun-names))
(setq fun-name (first fun-names))
(setq bodnam (get fun-name 'bodyname))
(setq genrlflag (member bodnam rep-bodies))
(cond ((member bodnam donebods) (spec-def fun-name
(getdef bodnam rep-defs)))
(t
(terpri)
(princ bodnam)
(princ '|? |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek)))
(setq nxtsym (ratom))
(do ()((not (eq nxtsym '?)))
(princ '|/
A function body is a set of horn clauses, terminated by a period./
/
body ::= horn-clauses "."/
/
horn-clauses ::= h-clause /| h-clause horn-clauses/
/
h-clause ::= goal "←" subgoals /| goal/
/
goal ::= fun-app/
/
subgoals ::= fun-app /| fun-app "," subgoals/
/
fun-app ::= name arglist /
/
For example:/
/
fact(0,1)/
fact(n,z) ← sub1(n,x), fact(x,z1), times(n,z1,z)/
|)
(terpri)
(princ bodnam)
(princ '|? |)
(setq nxtsym (ratom))
(cond ((eq nxtsym (implode (append
(explode bodnam)
'(?))))
(setq nxtsym (ratom)))))
(setq inpat (get fun-name 'inpat))
(putprop fun-name
(cond (genrlflag
(setq genrldef (repclauses))
(spec-def fun-name genrldef))
(t (repclauses)))
'body) )))) ;end of do collecting body-defs
(make-fundefs (rest (rest specs))))) ;end of conditional on bodies
(print 'end_of_generic_spec) (terpri) (terpri)
t) ;end first clause of cond
(t nil)))))
(def make-gendef (name sel-list)
(putprop name sel-list 'generic))
(def make-fundefs (fun-names)
(cond
((null fun-names) t)
(t
((lambda (x) (eval x)
(eval (list 'grindef (first fun-names))))
(translate (first fun-names) target))
(putprop (first fun-names) t 'function)
(terpri) (terpri)
(make-fundefs (rest fun-names)))))
(def splitbodies (bods ans)
(cond ((null bods) ans)
(t (splitbodies (rest bods)
(checkbod (first bods) ans)))))
(def checkbod (bodnam uniq-n-repeats)
(cond ((member bodnam (first uniq-n-repeats))
(list (first uniq-n-repeats)
(cons bodnam (second uniq-n-repeats))))
(t (list (cons bodnam (first uniq-n-repeats))
(second uniq-n-repeats)))))
(def getdef (name deflist)
(cond ((null deflist) (error
'(looking for a genrl definition that does no exist) name))
((eq name (first (first deflist)))
(rest (first deflist)))
(t (getdef name (rest deflist)))))
(def spec-def (fun-name genrldef)
(cons 'bktrkcond (spec-altlist (rest genrldef) (get fun-name 'inpat))))
(def spec-altlist (genalts inpat)
(cond ((null genalts) ())
(t ((lambda (matchlist)
(setq knownvars (known-of matchlist inpat))
(cons (list matchlist
(cons 'try (spec-goals (goal-pt (first genalts)))))
(spec-altlist (rest genalts) inpat)))
(match-pt (first genalts))))))
(def goal-pt (alternative) (rest (second alternative)))
(def spec-goals (gengoals)
(prog (tempgoal choices)
(return (cond ((null gengoals) ())
((setq choices
(is-generic (setq tempgoal (first gengoals))))
(cons (choosefun tempgoal choices)
(spec-goals (rest gengoals))))
(t (cons tempgoal (spec-goals (rest gengoals))))))))
(def formalize (arglist)
(cond ((null arglist) ())
((is-var (first arglist))
(cons (implode (cons '! (explode (first arglist))))
(formalize (rest arglist))))
(t (cons (first arglist) (formalize (rest arglist))))))
(def is-typedef ()
(cond ((eq nxtsym 'type)
(setq typename (read))
(terpri)
(setq params '(!x !y))
(setq inpat '(1 0))
(setq precond t)
(setq postcond '(boolean !y t))
(princ '|/
body?/ |)
(setq nxtsym (ratom))
(do () ((not (eq nxtsym '?)))
(princ '|/
For a type definition, the input pattern is always (1 0), the/
precondition is true, and the postcondition is that the output/
variable will have a boolean value./
/
A type body is a set of horn clauses,terminated by a/
period; it can be considered as the definition of a/
function to test for membership in the type. It /
always has a single input variable, which can be /
anything, and a single output variable, which is /
always truth-valued./
/
body ::= horn-clauses "."
/
horn-clauses ::= h-clause /| h-clause horn-clauses/
/
h-clause ::= goal "←" subgoals /| goal/
/
goal ::= fun-app/
/
subgoals ::= fun-app /| fun-app "," subgoals/
/
fun-app ::= name arglist /
/
For example:/
tree(empty-tree,y)/
tree( graft(t1,t2), y) ← tree(t1,y1), tree(t2,y2)/
|)
(terpri)(princ '|/
body?/ |)
(setq nxtsym (ratom)))
(setq body (repclauses)))
(t nil)))
(def put-types (l)
(cond ((null l) t)
(t (putprop (first l) typename 'typename)
(put-types (rest l)))))
.next page
;The following programs are for reading in precondition and postcondition
;specifications
(def readspec ()
(prog (disj)
(return (cond ((setq disj (is_disjunct)) disj)
(t (error (specification is not disjunction) nxtsym))))))
(def is_disjunct ()
(prog (conj1 conj2) (return
(cond ((setq conj1 (is_conjunct))
(do () ((not (eq nxtsym '∨)) conj1)
(setq nxtsym (ratom))
(cond ((setq conj2 (is_conjunct))
(setq conj1 (make_or conj1 conj2)))
(t (error '(∨ not followed by conjunct) nxtsym)))))
(t (error '(no conjunct to start with) nxtsym))))))
(def make_or (x y) (list '∨ x y))
(def make_and (x y) (list '∧ x y))
(def is_conjunct ()
(prog (lit1 lit2) (return
(cond ((setq lit1 (is_literal))
(do () ((not (eq nxtsym '∧)) lit1)
(setq nxtsym (ratom))
(cond ((setq lit2 (is_literal))
(setq lit1 (make_and lit1 lit2)))
(t (error '(∧ not followed by literal) nxtsym)))))
(t (error '(no literal to start with) nxtsym))))))
(def is_literal ()
(prog (atmf) (return
(cond ((or (eq nxtsym t) (eq nxtsym 'true)) (setq nxtsym (ratom)) t)
((eq nxtsym '/( ) (setq nxtsym (ratom))
(cond ((setq atmf (is_disjunct))
(cond ((eq nxtsym '/) )
(setq nxtsym (ratom))
atmf)
(t (error '(missing right paren) nxtsym))))
(t (error '(no disjunct in parens) nxtsym))))
(t (is_funapp))))))
.next page
;The following programs read in and internalize Horn clauses
(def repclauses ()
(cons 'bktrkcond (read_alternatives)))
; (cond ((reg-cond altlist) (cons 'cond altlist))
; (t (cons 'bktrkcond altlist))))
(def read_alternatives ()
(cond ((eq nxtsym '/.) ())
(t (cons (is_alternative) (read_alternatives)))))
;"←" should only appear in clauses which have something to the right of it
(def is_alternative ()
(do ()((not (eq nxtsym '?)))
(princ '|/
You are in the midst of specifying the body, a horn clause is looked for./
Don't forget that a single-goal clause does NOT have "←" following the goal,/
and the commas which separate subgoals are mandatory./
Here is a grammar description:/
/
horn-clauses ::= h-clause /| h-clause horn-clauses/
/
h-clause ::= goal "←" subgoals /| goal/
/
goal ::= fun-app/
/
subgoals ::= fun-app /| fun-app "," subgoals/
/
fun-app ::= name arglist /
/
|)
(terpri)(princ '|/
horn-clause?/ |)
(setq nxtsym (ratom)))
(cond ((setq goal (is_funapp))
(setq known-vars (known-of (rest goal) inpat))
(list (rest goal) (make_try (list_subgoals))))
(t (error '(bad goal) nxtsym))))
(def known-of (termlist pattern)
(cond ((null termlist) () )
((eq (first pattern) 1) (append (vars-in (first termlist))
(known-of (rest termlist)
(rest pattern))))
(t (known-of (rest termlist) (rest pattern)))))
(def vars-in (term)
(cond ( (atom term)
(cond ((is-var term)
(list term))
(t () )) )
( t (vars-in-list (rest term)))))
(def vars-in-list (termlist)
(cond ((null termlist) () )
(t (append (vars-in (first termlist))
(vars-in-list (rest termlist))))))
(def list_subgoals ()
(prog (tempgoal choices)
(return (cond ((eq nxtsym '←)
(setq nxtsym (ratom))
(setq tempgoal (is_funapp))
(cond ((and (not genrlflag)
(setq choices (is-generic tempgoal)))
(cons (choosefun tempgoal choices)(read_subgoals)))
((eq '%3∩%1 (first (explode (first tempgoal))))
(autopred (first tempgoal) (rest tempgoal))
(addoutvars tempgoal)
(cons tempgoal (read_subgoals)))
((not (null tempgoal))
(addoutvars tempgoal)
(cons tempgoal (read_subgoals)))
(t (error '(subgoal is not a funapp) nxtsym))))
(t ())))))
(def is-generic (call) (get (first call) 'generic))
(def addoutvars (call)
(do ((pat (get (first call) 'inpat) (rest pat))
(varlist (rest call) (rest varlist)))
((null pat))
(cond ((eq (first pat) 0)
(setq known-vars (append (vars-in (first varlist))
known-vars))))))
(def choosefun (call choicelist)
(prog (pat fun)
(setq pat (mk-pat (rest call)))
(setq fun (findfun pat choicelist))
(addoutvars (cons fun (rest call)))
(return (cons fun (rest call)))))
(def mk-pat (varlist)
(cond ((null varlist) () )
((is-constant (first varlist))
(cons 1 (mk-pat (rest varlist))))
((is-var (first varlist))
(cond ((memq (first varlist) known-vars)
(cons 1 (mk-pat (rest varlist))))
(t (cons 0 (mk-pat (rest varlist))))))
((all-vars-known (first varlist))
(cons 1 (mk-pat (rest varlist))))
(t (cons 0 (mk-pat (rest varlist))))))
(def findfun (key pairlist)
(cond ((null pairlist)
(princ '| /
i can't figure out which function you want from context, please help./
the patterns and function names you've given me are:/
|) (princ choicelist) (princ '|/
known-vars is: |) (princ known-vars) (princ '|/
which function do you want? |)
(read))
((as-defined-as key (first (first pairlist)))
(rest (first pairlist)))
(t (findfun key (rest pairlist)))))
(def as-defined-as (pat1 pat2)
(cond ((null pat1) t)
((and (eq (first pat1) 0) (eq (first pat2) 1)) nil)
(t (as-defined-as (rest pat1) (rest pat2)))))
(def all-vars-known (exp)
(cond ((atom exp) (or (is-constant exp)
(memq exp known-vars)))
(t (all-vars-in-list-known (rest exp)))))
(def all-vars-in-list-known (l)
(cond ((null l) t)
((all-vars-known (first l))
(all-vars-in-list-known (rest l)))
(t nil)))
(def make_match (x y) (list 'match x y))
(def make_try (l) (cons 'try l))
(def read_subgoals ()
(prog (tempgoal choices)
(return (cond ((eq nxtsym '/,)
(setq nxtsym (ratom))
(setq tempgoal (is_funapp))
(cond ((and (not genrlflag)
(setq choices (is-generic tempgoal)))
(cons (choosefun tempgoal choices)(read_subgoals)))
((eq '%3∩%1 (first (explode (first tempgoal))))
(autopred (first tempgoal) (rest tempgoal))
(addoutvars tempgoal)
(cons tempgoal (read_subgoals)))
((not (null tempgoal))
(addoutvars tempgoal)
(cons tempgoal (read_subgoals)))
(t (error '(subgoal is not a funapp) nxtsym))))
(t ())))))
(def is-constant (x)
(cond ((atom x) (or (numberp x)
(eq x t)
(eq x 'f)
(eq x 'true)
(eq x 'undef)
(eq x 'false)
(eq x nil)))
(t (or (not (is-string x)) (eq (first x) 'quote)
(not (contains-var x))))))
(def is-var (x) (and (atom x) (not (is-constant x))))
(def contains-var (exp)
(cond ((atom exp) (is-var exp))
(t (list-contains-var (rest exp)))))
;contains-var ignores function names when looking for variables since the only
;functions left in at this point are constructors
(def list-contains-var (explist)
(cond ((null explist) nil)
((contains-var (first explist)) t)
(t (list-contains-var (rest explist)))))
.next page
;The following programs perform the translation to target language
(def translate (name target)
(cond ((eq target 'lisp)
(make_lisp_def))
((eq target 'pascal)
(mk-strong-typed)
(make_pascal_def))
(t (error '(language not yet implemented) target))))
(def make_lisp_def () (list 'defun name 'fexpr '(l)
(list 'cond (list
(list 'true-precond (list 'cons
(list 'quote
name)
'l))
(list 'bktrkcond
'l
(list 'quote (rest body))))
'(t 'undef))))
(def mk-strong-typed ()
(make-formal-types (get name 'params) ;this function puts the formal params
(get name 'precond) ;and their types under 'types, and
(get name 'postcond) ;deletes the type decs from the pre-
name) ;and post-conditions, putting the
;results under 'typedprecond and
;typedpostcond
(putprop name (findprocs (rest (get name 'body)) name) 'external-procs)
(putprop name (find-local-types (rest (get name 'body)) name) 'local-decs))
(def make-formal-types (params precond postcond name)
((lambda (split-pre split-post)
(putprop name (mk-param-types params
(append (first split-pre)
(first split-post)))
'types)
(putprop name (rest split-pre) 'typedprecond)
(putprop name (rest split-post) 'typedpostcond))
(findtypes precond)
(findtypes postcond)))
(def mk-param-types (params types)
(cond ((null params) ())
(t ((lambda (ans)
(cond ((defined ans)
(cons ans (mk-param-types (rest params)
types)))
(t (error '(has no type defined) (first params)))))
(lookup (first params) types)))))
(def lookup (var alist)
(cond ((null alist) 'undef)
((eq var (first (first alist)))
(rest (first alist)))
(t (lookup var (rest alist)))))
(def findtypes (precond) ;returns the dotted-pair: list of var-type pairs,
(cond ((atom precond) ;and non-type-dec part of precond
(cons () precond))
((is-or precond)
(error '(no ∨'s allowed in preconditions when translating
to strongly typed languages) precond))
;if we switch from dnf to cnf, then we can allow ∨'s to appear
;in pre- and post-conditions, but no type decs may be ∨'ed, the
;alternative replacing the error above would be:
;(cons () precond)
((is-and precond)
((lambda (rest-ans1 rest-ans2)
(cons (append (first rest-ans1)
(first rest-ans2))
(list '∧ (rest rest-ans1)
(rest rest-ans2))))
(findtypes (second precond))
(findtypes (third precond))))
((is-type (first precond)) ;we know that the first
(cons (list (cons (second precond) ;argument of a type
(first precond))) ;app. is the input var
T))))
(def is-type (name)
(or (get name 'type)
(memq name prim-types)))
(def findprocs (alts name)
(cond ((null alts) ())
(t (append (findcalls (try-pt (first alts)) name)
(findprocs (rest alts) name)))))
(def findcalls (sbgls name)
(cond ((null sbgls) ())
(t ((lambda (procname)
(cond ((eq procname name)
(findcalls (rest sbgls) name))
(t (cons procname (findcalls (rest sbgls) name)))))
(first (first sbgls))))))
(def find-local-types (alts name)
(cond ((null alts) ())
(t (append (findtypesfor (try-pt (first alts)) name)
(find-local-types (rest alts) name)))))
(def findtypesfor (sbgls name)
(cond ((null sbgls) ())
(t ((lambda (sbgl)
(cond ((eq (first sbgl) name)
(findtypesfor (rest sbgls) name))
(t (append (make-type-list (rest sbgl)
(get (first sbgl) 'types))
(findtypesfor (rest sbgls) name)))))
(first sbgls)))))
(def make-type-list (actuals type-pattern) ;returns a list of var-type pairs
(cond ((nul actuals) ())
((is-var (first actuals))
(cons (cons (first actuals)
(first type-pattern))
(make-type-list (rest actuals)
(rest type-pattern))))
((is-constant (first actuals))
(make-type-list (rest actuals)
(rest type-pattern)))
(t (append ;it's a funapp, i.e., a constructed type, so
(hard-type-list (first actuals) ;lookup def of type and make
(first type-pattern)) ;sure the constructor
(make-type-list (rest actuals) ;is appropriate, then find
(rest type-pattern)))))) ;types of the args
(def hard-type-list (exp type)
(cond ((eq (vars-in exp) ()) ())
(t ((lambda (bod)
(cond (bod (srch-alts (list exp (gensym)) ;assumes inpat (1 0)
(rest bod)))
(t (error '(has not yet been defined) type))))
(get type 'body)))))
(def srch-alts (actuals list-alts)
(cond ((null list-alts) (error '(has vars whose types I am unable to determine)
(first actuals)))
(t ((lambda (sbgls)
(cond ((defined sbgls)
((lambda (typedecs)
(cond ((null typedecs)
(srch-alts actuals
(rest list-alts)))
(t ((lambda (ans)
(cond ((all-typed
(vars-in (first actuals))
ans)
ans)
(t (srch-alts actuals
(rest list-alts)))))
(find-var-types
(vars-in (first actuals))
(append (first sbgls)
typedecs))))))
(find-type-decs (rest sbgls))))
(t (srch-alts actuals (rest list-alts)))))
(half-eval actuals (first list-alts))))))
(def half-eval (actuals alt) ;returns a substitution and list of subgoals with the
((lambda (sub) ;substitutions made
(cond ((defined sub)
(cons sub (mk-subst (try-pt alt) sub)))
(t 'undef)))
(match actuals (match-pt alt))))
(def find-type-decs (sbgls)
(cond ((null sbgls) ())
(t ((lambda (sbgl)
(cond ((is-type (first sbgl))
(append (make-type-list (list (second sbgl))
(list (first sbgl)))
(find-type-decs (rest sbgls))))
(t (find-type-decs (rest sbgls)))))
(first sbgls)))))
(def find-var-types (vars sub)
(cond ((null vars) ())
(t (cons (cons (first vars)
(lookup* (first vars) sub))
(find-var-types (rest vars) sub)))))
(def all-typed (vars alist)
(cond ((null vars) t)
((is-type (lookup (first vars) alist))
(all-typed (rest vars) alist))
(t nil)))
.next page
.ss(Listing of LISP Implementation,,P13:)
.P9:
;primitive function and type definitions
;for LISP
(PROG2
(putprop 'lisp '( (def integer fexpr (l)
(cond ((eq (length l) 1)
(cond ((fixp (first l)) ())
(t 'undef)))
((is-constant (second l))
(cond ((fixp (first l))
(cond ((or (eq (second l) 'true)
(eq (second l) t)) () )
(t 'undef)))
((or (eq (second l) 'undef)
(eq (second l) 'false)) ())
(t 'undef)))
(t (list (cons (second l)
(cond ((fixp (first l)) t)
(t 'false)))))))
(def real fexpr (l)
(cond ((eq (length l) 1)
(cond ((floatp (first l)) ())
(t 'undef)))
((is-constant (second l))
(cond ((floatp (first l))
(cond ((or (eq (second l) 'true)
(eq (second l) t)) () )
(t 'undef)))
((or (eq (second l) 'undef)
(eq (second l) 'false)) ())
(t 'undef)))
(t (list (cons (second l)
(cond ((floatp (first l)) t)
(t 'false)))))))
(def boolean fexpr (l)
(cond ((eq (length l) 1)
(cond ((or (eq (first l) t)
(eq (first l) 'true)
(eq (first l) 'undef)
(eq (first l) 'false)) ())
(t 'undef)))
((is-constant (second l))
(cond ((or (eq (first l) t)
(eq (first l) 'true)
(eq (first l) 'undef)
(eq (first l) 'false))
(cond ((or (eq (second l) 'true)
(eq (second l) t)) () )
(t 'undef)))
((or (eq (second l) 'undef)
(eq (second l) 'false)) ())
(t 'undef)))
(t (list (cons (second l)
(cond
((or (eq (first l) t)
(eq (first l) 'true)
(eq (first l) 'undef)
(eq (first l) 'false)) t)
(t 'false)))))))
(def ≤ fexpr (l)
(cond ((eq (length l) 2)
(cond ((or (old< (first l) (second l))
(old= (first l) (second l))) ())
(t 'undef)))
((is-constant (third l))
(cond ((or (old< (first l) (second l))
(old= (first l) (second l)))
(cond ((or (eq (third l) t)
(eq (third l) 'true)) ())
(t 'undef)))
((or (eq (third l) 'false)
(eq (third l) 'undef))())
(t 'undef)))
(t (list (cons (third l)
(cond ((or (old< (first l) (second l))
(old= (first l) (second l)))
t)
(t 'false)))))))
(def ≥ fexpr (l)
(cond ((eq (length l) 2)
(cond ((or (old> (first l) (second l))
(old= (first l) (second l))) ())
(t 'undef)))
((is-constant (third l))
(cond ((or (old> (first l) (second l))
(old= (first l) (second l)))
(cond ((or (eq (third l) t)
(eq (third l) 'true)) ())
(t 'undef)))
((or (eq (third l) 'false)
(eq (third l) 'undef))())
(t 'undef)))
(t (list (cons (third l)
(cond ((or (old> (first l) (second l))
(old= (first l) (second l)))
t)
(t 'false)))))))
(def ≠ fexpr (l)
(cond ((eq (length l) 2)
(cond ((old= (first l) (second l)) 'undef)
(t ())))
((is-constant (third l))
(cond ((old= (first l) (second l))
(cond ((or (eq (third l) 'undef)
(eq (third l) 'false)) ())
(t 'undef)))
((or (eq (third l) 'true)
(eq (third l) t))())
(t 'undef)))
(t (list (cons (third l)
(cond ((old= (first l) (second l))
'false)
(t t)))))))
(putprop 'old< (get '< 'subr) 'subr)
(putprop 'old> (get '> 'subr) 'subr)
(putprop 'old= (get '= 'subr) 'subr)
(def < fexpr (l)
(cond ((eq (length l) 2)
(cond ((old< (first l) (second l)) ())
(t 'undef)))
((is-constant (third l))
(cond ((old< (first l) (second l))
(cond ((or (eq (third l) 'true)
(eq (third l) t)) ())
(t 'undef)))
((or (eq (third l) 'false)
(eq (third l) 'undef)) ())
(t 'undef)))
(t (list (cons (third l)
(cond ((old< (first l) (second l)) t)
(t 'false)))))))
(def ∨ fexpr (l)
(cond ((eq (length l) 2)
(cond ((or (first l) (second l)) ())
(t 'undef)))
((is-constant (third l))
(cond ((or (first l) (second l))
(cond ((or (eq (third l) 'true)
(eq (third l) t)) ())
(t 'undef)))
((or (eq (third l) 'undef)
(eq (third l) 'false)) ())
(t 'undef)))
(t (list (cons (third l)
(cond ((or (first l) (second l)) t)
(t 'false)))))))
(def ∧ fexpr (l)
(cond ((eq (length l) 2)
(cond ((and (first l) (second l)) ())
(t 'undef)))
((is-constant (third l))
(cond ((and (first l) (second l))
(cond ((or (eq (third l) 'true)
(eq (third l) t)) ())
(t 'undef)))
((or (eq (third l) 'undef)
(eq (third l) 'false)) ())
(t 'undef)))
(t (list (cons (third l)
(cond ((and (first l) (second l)) t)
(t 'false)))))))
(def > fexpr (l)
(cond ((eq (length l) 2)
(cond ((old> (first l) (second l)) ())
(t 'undef)))
((is-constant (third l))
(cond ((old> (first l) (second l))
(cond ((or (eq (third l) 'true)
(eq (third l) t)) ())
(t 'undef)))
((or (eq (third l) 'false)
(eq (third l) 'undef)) ())
(t 'undef)))
(t (list (cons (third l)
(cond ((old> (first l) (second l)) t)
(t 'false)))))))
(def = fexpr (l)
(cond ((eq (length l) 2)
(cond ((old= (first l) (second l)) ())
(t 'undef)))
((is-constant (third l))
(cond ((old= (first l) (second l))
(cond ((or (eq (third l) 'true)
(eq (third l) t)) ())
(t 'undef)))
((or (eq (third l) 'false)
(eq (third l) 'undef)) ())
(t 'undef)))
(t (list (cons (third l)
(cond ((old= (first l) (second l)) t)
(t 'false)))))))
; (def + (x y) (+ x y)) these functions are already
; (def - (x y) (- x y)) defined properly, they are listed
; (def * (x y) (* x y)) here just to indicate we didn't
; (def // (x y) (// x y)) forget them
(def r+ (x y) (+$ x y))
(def r- (x y) (-$ x y))
(def r* (x y) (*$ x y))
(def r// (x y) (//$ x y))
;stuff for adding strings which are represented as a list of 2 elements,
; the first is the atom STRING, the second is a list of the characters in the
; string.
(def readstring ()
(prog (temp hdr)
(setq temp (cons (readch) () ))
(setq hdr (cons temp temp))
(return (do ((nxtchar (readch) (readch)))
((and (eq nxtchar '")
(not (eq (tyipeek) 42)))
(list 'string (car hdr)))
(cond ((eq nxtchar '")(readch)))
(setq temp (cons nxtchar () ))
(rplacd (cdr hdr) temp)
(rplacd hdr temp)))))
(def string fexpr (l) (cons 'string l))
(setsyntax '" 'macro 'readstring)
(putprop 'prt (get 'print 'subr) 'subr)
(def print (x)
(cond ((or (atom x) (not (eq (first x) 'string)))
(prt x))
(t (prt (maknam (second x))))))
(def is-string fexpr (x)
(cond ((eq (length x) 1)
((lambda (y)
(cond
((and (not (atom y))
(eq (first y) 'string)
(null (rest (rest y)))) ())
(t 'undef)))
(eval (first x))))
(t ((lambda (y1 y2)
(cond
((and (not (atom y1))
(eq (first y1) 'string)
(null (rest (rest y1))))
(cond ((or (eq y2 'true)
(eq y2 t)) ())
((or (eq y2 'false)
(eq y2 'undef)) 'undef)
(t (list (cons y2 t)))))
((or (eq y2 'false)
(eq y2 'undef)) ())
((or (eq y2 'true)
(eq y2 t)) 'undef)
(t (list (cons y2 'false)))))
(eval (first x))
(second x)))))
(def s-cat (x y)
(cond ((not (is-string x))
(error '(s-cat applied to non-string) x))
((not (is-string y))
(error '(s-cat applied to non-string) y))
(t (list 'string (append (second x) (second y))))))
(def firstch (x)
(cond ((not (is-string x)) (error '(firstch of non-string)x))
((atom (second x)) (error '(firstch of emptystring)x))
(t (first (second x)))))
(def tail (x)
(cond ((not (is-string x)) (error '(tail of non-string) x))
((atom (second x)) (error '(tail of emptystring)x))
(t (list 'string (rest (second x))))))
(def s-cons (x y)
(cond ((not (eq (flatc x) 1)) (error '(bad character object/, s-cons) x))
((not (is-string y)) (error '(s-cons of non-string) y))
(t (list 'string (cons x (second y))))))
(def mk-string (x) (cond ((not (eq (flatc x) 1)) (error '(mk-string of non-character)
x))
(t (list 'string (cons x () )))))
(def is-list (l)
(cond ((atom l) (eq l nil))
(t (is-list (rest l)))))
(def firstsym fexpr (l) (matchterms (second l) (list 'quote (ratom))))
(def firstexp fexpr (l) (matchterms (second l) (read)))
(def write (x) (print x) ())
)
'primdefs)
NIL) ;end of prog surrounding all the primitive definitions
.P8:
;the following include all definitions needed for lisp to run generated programs
(def bktrkcond (actuals list-alts)
(cond ((null list-alts) 'undef)
(t ((lambda (alt)
((lambda (answer-sub)
(cond ((defined answer-sub)
(cleanup answer-sub actuals))
(t (bktrkcond actuals (rest list-alts)))))
((lambda (sub)
(cond ((defined sub)
(append-if-defined sub
(try (mk-subst (try-pt alt)
sub))))
(t 'undef)))
(match actuals (match-pt alt)))))
(new-version (first list-alts))))))
(def new-version (alt)
((lambda (sub)
(list (mk-subst (match-pt alt) sub)
((lambda (newtry)
(cons 'try (mk-subst newtry (chg-formals newtry))))
(mk-subst (try-pt alt) sub))))
(chg-in (match-pt alt))))
(def chg-formals (sbgoals)
(cond ((null sbgoals) ())
(t ((lambda (x) (cond (x (append x (chg-formals (mk-subst
(rest sbgoals)
x))))
(t (chg-formals (rest sbgoals)))))
(chg-in (rest (first sbgoals)))))))
(def chg-in (params)
(cond ((null params) ())
((atom (first params))
(cond
((eq (firstchar (first params)) '!)
((lambda (chg) (cons chg (chg-in (subst (cdr chg)
(car chg)
(rest params)))))
(cons (first params) (gensym))))
(t (chg-in (rest params)))))
((eq (first (first params)) 'quote)
(chg-in (rest params)))
(t ((lambda (chgs)
(append chgs (chg-in (mk-subst (rest params) chgs))))
(chg-in (rest (first params)))))))
(def firstchar (name)
(first (explode name)))
(def cleanup (sub actuals) (reverse (cleanup* sub actuals () )))
(def cleanup* (sub actuals ans)
(cond ((null actuals) ans)
(t ((lambda (act)
(cond ((is-var act)
(cond ((already-there act ans)
(cleanup* sub (rest actuals) ans))
(t (cleanup* sub (rest actuals)
(cons (cons act
(lookup* act sub))
ans)))))
((is-constant act)
(cleanup* sub (rest actuals) ans))
(t (cleanup* sub (rest actuals)
(cleanup* sub (rest act) ans)))))
(first actuals)))))
(def already-there (name alist)
(cond ((null alist) nil)
((eq name (var (first alist))) t)
(t (already-there name (rest alist)))))
(def lookup* (exp alist) ;makes all substitutions in alist that are
(do ((value (mk-subst exp alist) nxtval) ;applicable to exp
(nxtval (mk-subst (mk-subst exp alist) alist)
(mk-subst nxtval alist)) )
((equal value nxtval) value)))
(def try (subgoals)
(cond ((null subgoals) () )
(t
( (lambda (sub)
(cond ((defined sub)
(append-if-defined sub
(try (mk-subst
(rest subgoals)
sub))))
(t 'undef)))
(eval (first subgoals)) ))
))
(def append-if-defined (sub1 sub2) ;when used in conjunction
(cond ((and (defined sub1) (defined sub2)) ;with "try", this involves
(append sub1 sub2)) ; a redundant test on the
(t 'undef))) ;first argument (who cares?)
(def true-precond (fnapp)
(prog (env2 ans-sub)
(setq env2 (bind (matchlis (first fnapp)) (rest fnapp)))
(setq ans-sub (evpred (mk-subst (get (first fnapp) 'precond) env2)))
(return (cond ((eq ans-sub ()) t)
((eq ans-sub 'undef) nil)
(t (error '(variables in precond check) ans-sub))))))
;precondition checker - evpred evaluates wffs
(def evpred (f)
(cond ((atom f) (cond ((eq f t) ())
((eq f nil) (error '(no precondition exists for)
(first fnapp)))
(t (error '(weird atomic predicate)f))))
((is-or f) (evor (rest f)))
((is-and f) (evand (rest f)))
;otherwise it is a pred-app
(t (eval f))))
(def is-or (f) (eq (first f) '∨))
(def evor (l) (prog (val)
(setq val (evpred (first l)))
(return (cond ((eq 'undef val) (evpred (second l)))
((eq () val) ())
(t (evpred (second l))) ;who knows, we might as well let 'em try
(t (error '(evpred evaluates to something other than () or undef)
(cons val (first l))))))))
(def is-and (f) (eq (first f) '∧))
(def evand (l) (prog (val)
(setq val (evpred (first l)))
(return (cond ((eq val ()) (evpred (second l)))
((eq val 'undef) 'undef)
(t (error '(evpred evaluates to weirdness) (cons val (first l))
))))))
(def defined (x) (not (eq x 'undef)))
;bind is here creating an alist, (a list of "(var.value)" pairs)
(def bind (l1 l2)
(cond ((null l1) ())
(t (cons (cons (first l1) (first l2)) (bind (rest l1) (rest l2))))))
(def matchlis (fname) (get fname 'params))
(def match (l1 l2)
(prog (termatch)
(return (cond ((null l1) (cond ((null l2) ())
(t (error '(tried to match lists of unequal length)l2
))))
(t (setq termatch (matchterms (first l1) (first l2)))
(prog (restmatch)
(return
(cond ((null termatch) (match (rest l1) (rest l2)))
((eq termatch 'undef) 'undef)
((defined
(setq restmatch
(match (mk-subst (rest l1) termatch)
(mk-subst (rest l2) termatch))))
(append termatch restmatch))
(t 'undef)))) )))))
(def mk-subst (termlist alist) ;actually, termlist can be
(cond ((and (atom termlist)
(or (numberp termlist)
(eq termlist t)
(eq termlist 'f)
(eq termlist 'true)
(eq termlist 'undef)
(eq termlist 'false)
(eq termlist nil)))
termlist)
((and (not (atom termlist))
(or (not (is-string termlist)) (eq (first termlist) 'quote)))
termlist)
(t
(do ((l alist (rest l))
(exp termlist (subst (val (first l)) (var (first l)) exp)))
((null l) exp)))))
(def val (x) (cdr x))
(def var (x) (car x))
;all variables occurring in the terms to be matched are unbound, as substitutions
;are made as we go
(def matchterms (t1 t2)
(prog (f)
(return (cond ((equal t1 t2) ())
((atom t1) (cond ((is-var t1) (cond ((or (eq(is-string t2)())
(atom t2)) (cons
(cons t1 t2)
() ))
((occurs-in t1 t2)
(cond ((get
(setq f
(implode (append
(explode
'equal-bind-)
(explode
(get (first t2)
'typename)))))
'body)
(f t1 t2))
(t 'undef)))
(t (cons (cons t1 t2) ()))))
(t (cond ((is-var t2) (cons (cons t2 t1) ()))
((is-constant t1)
(cond ((atom t2) 'undef)
((and (eq (first t2) 'quote)
(eq (second t2) t1))
())
(t 'undef)))
((is-constant t2) 'undef)
((contains-var t2) (cond
((get
(setq f
(implode (append
(explode
'equal-bind-)
(explode
(get (first t2)
'typename)))))
'body)
(f t1 t2))
(t 'undef)))
((get
(setq f (implode (append
(explode
'equal-)
(explode
(get (first t2)
'typename)))))
'body)
(cond ((f t1 t2) ())
(t 'undef)))
(t 'undef)))))
((is-var t2) (cond
((eq (is-string t1) ())
(cons (cons t2 t1) () ))
((occurs-in t2 t1)
(cond ((get
(setq f
(implode (append
(explode
'equal-bind-)
(explode
(get (first t1)
'typename)))))
'body)
(f t1 t2))
(t 'undef)))
(t (cons (cons t2 t1) ()))))
((and (atom t2) (is-constant t2))
(cond ((and (eq (first t1) 'quote)
(eq (second t1) t2))
())
(t 'undef)))
((get (setq f (implode (append (explode 'equal-)
(explode (get (first t1)
'typename)))))
'body)
(cond ((f t1 t2) ())
(t 'undef)))
((or (and (not (eq (is-string t1) ()))(contains-var t1))
(and (not (eq (is-string t2) ()))(contains-var t2)))
(cond ((get (setq f (implode (append
(explode
'equal-bind-)
(explode
(get (first t1)
'typename)))))
'body)
(f t1 t2))
((and (eq (first t1) (first t2)) (not (eq (first t1) 'quote)))
(match (rest t1) (rest t2)))
((eq (first t1) 'list)
(matchterms (cons-out (rest t1)) t2))
((eq (first t2) 'list)
(matchterms (cons-out (rest t2)) t1))
((eq (first t1) 'cons)
(cond ((eq (first t2) 'quote)
((lambda (x)
(cond
((defined x)
((lambda (y)
(cond
((defined y)
(append x y))
(t 'undef)))
(matchterms
(mk-subst (third t1) x)
(list 'quote
(rest (second t2)) ))))
(t 'undef)))
(matchterms (second t1)
(list 'quote
(first (second t2))))))
(t
((lambda (x)
(cond
((defined x)
((lambda (y)
(cond
((defined y)
(append x y))
(t 'undef)))
(matchterms
(mk-subst (third t1) x)
(mk-subst (rest t2) x))))
(t 'undef)))
(matchterms (second t1) (first t2))))))
((eq (first t2) 'cons)
(cond ((eq (first t1) 'quote)
((lambda (x)
(cond
((defined x)
((lambda (y)
(cond
((defined y)
(append x y))
(t 'undef)))
(matchterms
(mk-subst (third t2) x)
(list 'quote
(rest (second t1)) ))))
(t 'undef)))
(matchterms (second t2)
(list 'quote
(first (second t1))))))
(t
((lambda (x)
(cond
((defined x)
((lambda (y)
(cond
((defined y)
(append x y))
(t 'undef)))
(matchterms
(mk-subst (third t2) x)
(mk-subst (rest t1) x))))
(t 'undef)))
(matchterms (second t2) (first t1))))))
(t 'undef)))
(t 'undef)))))
(def cons-out (l)
(cond ((null l) ())
(t (list 'cons (first l) (cons-out (rest l))))))
(def contains-var (exp)
(cond ((atom exp) (is-var exp))
(t (list-contains-var (rest exp)))))
;contains-var ignores function names when looking for variables since the only
;functions left in at this point are constant functions (arithmetic and constructors)
(def list-contains-var (explist)
(cond ((null explist) nil)
((contains-var (first explist)) t)
(t (list-contains-var (rest explist)))))
(def occurs-in (var exp)
(cond ((atom exp) (cond ((eq var exp) t)
(t nil)))
((occurs-in var (first exp)) t)
(t (occurs-in var (rest exp)))))
(def match-pt (alternative) (first alternative))
(def try-pt (alternative) (rest (second alternative)))
;*** automatic predicatizing ***
(def autopred (f varlist)
(cond
((get f 'body) nil) ;it's already defined, go away
(t
(putprop f (mk-params varlist) 'params)
(putprop f t 'precond) ;using system defined functions relys on the
(putprop f (invent-pat varlist) 'inpat)
(putprop f t 'postcond)
(putprop f (mk-predbody f varlist) 'body))))
(def mk-params (varlist)
(do ((ct varlist (rest ct))
(l () (cons (intern (gensym)) l)))
((null ct) l)))
(def mk-predbody (f varlist)
(prog (namestring)
(setq namestring (explode f))
(return (cond ((eq (second namestring) 'f)
(eval (list 'defun f 'fexpr '(argl)
(list 'prog '(seplist outpos)
'(setq seplist (split argl))
'(setq outpos (second seplist))
(list 'return
(list 'cond
(list '(is-var outpos)
(list 'list
(list 'cons
'outpos
(list 'eval
(list 'cons
(list 'quote
(cond
((eq (third namestring) '//)
(implode (rest (rest (rest namestring)))))
(t
(implode
(rest (rest
namestring))
))) )
'(first seplist))) )))
(list (list
'equal
'outpos
(list 'eval
(list 'cons
(list 'quote
(cond
((eq (third namestring) '//)
(implode (rest (rest (rest namestring)))))
(t
(implode
(rest (rest
namestring))
))) )
'(first seplist))) )
() )
(list t ''undef) ))))))
((eq (second namestring) 'p)
(eval (list 'defun f 'fexpr '(argl)
(list 'prog '(seplist ans)
'(setq seplist (split argl))
(list 'setq
'ans
(list 'eval
(list 'cons
(list 'quote
(implode
(rest (rest
namestring))
))
'(first seplist))))
'(return
(cond
((is-var (second seplist))
(list (cons (second seplist)
ans)))
((equal ans (second seplist))
() )
(t 'undef)))
))) )
(t (error '(autopred called w/no %3∩%1p or %3∩%1f) f))))))
(def split (l) (cond ((null l) (error '(request to split empty list)l))
((null (rest l)) (list () (first l)))
(t ((lambda (h) (cons (cons (first l) (first h))
(rest h)))
(split (rest l))))))
(def invent-pat (varlist)
(do ((ct (rest varlist) (rest ct))
(pat (cons 0 () ) (cons 1 pat)))
((null ct) pat)))
.end
.ss(Listing of Pascal Implementation,,P14:)
.begin nofill;turn off "↑"
.P12:
;lisp programs for generating pascal
;each function specification gets turned into a complete program so that
;a library of functions can be built. Each function is declared external.
;the surrounding program is just a dummy to satisfy syntax restrictions.
;a type specification is turned into a type declaration and stuffed on the
;property list of the type name(under 'type-dec), to be
;included in the declaration of every
;function that uses the type. (apparently there is no such thing as an
;external type in pascal, so it has to be re-declared everywhere)
(def make_pascal_def ()
(append
(list 'program '/ (gensym) '/, name '/; '/
)
(make-type-decs) ;makes the definitions for all types used
;i.e., termlists, terms, constants, symbols,
; and whatever else is necessary as subtypes
(make-external-decs (get name 'external-procs))
(list 'function '/ name (rest (make-parameter-list
(strip! (get name 'params))
(get name 'inpat)))
': '/ 'boolean '/; '/
)
(make-body-of name);dont forget to include: new(actuals);
(list 'begin '/ ; actuals↑.sl := true;
'end '/.)
))
(def strip! (varlist)
(cond ((null varlist) ())
(t (cons ((lambda (namelist)
(cond ((eq (first namelist) '!)
(implode (rest namelist)))
(t (first varlist))))
(explode (first varlist)))
(strip! (rest varlist))))))
(def make-parameter-list (params inpat) ;declares all formals to be type term, but
(cond ((null params)()) ;leaves an extra ";" on the
(t (append ; front of the list
((lambda (arg)
((lambda (first-dec)
(cond ((eq (first inpat) 0)
(append '(/; var) first-dec))
(t (cons '/; first-dec))))
(list arg ': 'term)))
(first params))
(make-parameter-list (rest params) (rest inpat))))))
;every formal parameter is of type TERM
;every local used by the spec must be of type TERM
(def make-local-decs (locals) ;takes a 4 element list of vars to be declared as
(append '(var /
;termlists, terms, constants, and
) ;symbols, and returns a list that
(cons '/ (rest ;consists of the pascal to do it
(rest (make-decs (first locals)
'termlist))))
(cons '/ (rest
(rest (make-decs (second locals)
'term))))
(cond ((null (third locals)) ()) (t
(cons '/ (rest
(rest (make-decs (third locals)
'constant))))))
(cond ((null (fourth locals)) ()) (t
(cons '/ (rest
(rest (make-decs (fourth locals)
'symbol))))))))
(def make-decs (vars type) ;makes a list of vars : type, leaves an extra ","
(cond ((null vars) (list ': '/ type'/;'/
)) ;and " " on front
(t (append (list '/, '/ (first vars))
(make-decs (rest vars) type)))))
(def make-type-decs ()
'(type /
/ alltyps / = / /( integertyp /, realtyp /, booleantyp /,
chartyp /, symboltyp /) /; /
/
/ termtyps / =/ /( variable /, / constanttyp /, / funapp /)/;/
/
/ term / =/ ↑t1 /;/
/
/ termlist/ =/ ↑tl1/;/
/
/ constant/ =/ ↑c1/;/
/
/ symbol/ =/ ↑sym1/;/
/
/ t1/ =/ record/
/ / case / ttyp:termtyps / of/
/ / / variable:/ /(vr:/ integer/)/;/
/ / / constanttyp:/ /(cnst:/ constant/)/;/
/ / / funapp:/ /(fname:/ symbol/;/
/ / / / / args:/ termlist/)/
/ / end/;/
/
/ tl1/ =/ record/
/ / notempty:/ boolean/;/
/ / first:/ term/;/
/ / rest:/ termlist/
/ / end/;/
/
/ c1/ =/ record/
/ / case/ ctyp:alltyps/ of/
/ / / integertyp:/ /(ival:/ integer/)/;/
/ / / realtyp:/ /(rval:/ real/)/;/
/ / / booleantyp:/ /(bval:/ boolean/)/;/
/ / / chartyp:/ /(cval:/ char/)/;/
/ / / symboltyp:/ /(sval:/ symbol/)/
/ / end/;/
/
/ sym1/ =/ record/
/ / notempty:/ boolean/;/
/ / firstch:/ char/;/
/ / tail:/ symbol/;/
/ / end/;/
/
/ varpairs/ =/ ↑vp/;/
/
/ vp/ =/ record/
/ / notempty:/ boolean/;/
/ / old:/ integer/;/
/ / new:/ integer/;/
/ / rest:/ varpairs/
/ / end/;/
/
))
(def cons-if-new (x l)
(cond ((memq x l) l)
(t (cons x l))))
(def general-funs ()
'(function / occur(x/,/ y:/ term):/ boolean/;/
/ extern/;/
function/ genvar:/ integer/;/
/ extern/;/
procedure / replace(x/,/ t:/ term/;/ var/ tml:/ termlist)/;/
/ extern/;/
procedure/ subst(x/,/ t:/ term/;/ var/ t1/,/ t2:/ termlist)/;/
/ extern/;/
function/ eqsym(x/,/ y:/ symbol):/ boolean/;/
/ extern/;/
function/ eqconst(x/,/ y:/ constant):/ boolean/;/
/ extern/;/
function/ copysym(oldsym:/ symbol):/ symbol/;/
/ extern/;/
function/ copyterm(oldtm:/ term):/ term/;/
/ extern/;/
function/ copytermlist(tml:/ termlist):/ termlist/;/
/ extern/;/
function/ copyconst(oldconst:/ constant):/ constant/;/
/ extern/;/
function/ unify(var/ x/,y/,allx/,ally:termlist/;failed:boolean):/ boolean/;/
/ extern/;/
procedure/ Lookup(tm:/ term/;/ tbl:/ varpairs/;/ found:/ boolean)/;/
/ extern/;/
procedure/ Standapart(tml:/ termlist/;/ var/ donetbl:/ varpairs)/;/
/ extern/;/
))
(def make-external-decs (procnames)
(cond ((null procnames) (general-funs))
(t (append (mk-ext-dec (first procnames))
(make-external-decs (rest procnames))))))
(def mk-ext-dec (name)
((lambda (x)
(cond (x x)
(t (putprop name (list 'FUNCTION '/ name
(make-parameter-list (get name 'types)
(get name 'inpat))
': '/ 'boolean '/; '/
'/ 'EXTERN '/; '/
)
'extproc-head))))
(get name 'extproc-head)))
(def algol-ize (wff)
(cond ((atom wff) 'true)
((eq (first wff) '∧)
((lambda (arg1 arg2)
(cond ((eq arg1 'true) (cond ((eq arg2 'true) 'TRUE)
(t arg2)))
((eq arg2 'true) arg1)
(t (list arg1 'AND arg2))))
(algol-ize (second wff))
(algol-ize (third wff))))
((eq (first wff) '∨)
((lambda (arg1 arg2)
(cond ((eq arg1 'true) 'TRUE)
((eq arg2 'true) 'TRUE)
(t (list arg1 'OR arg2))))
(algol-ize (second wff))
(algol-ize (third wff))))
(t ((lambda (ans-code) ;o.w. it is a funapp, so generate
(setq pascode (append pascode ;pascal to represent the
(rest ans-code))) ;terms and build the
(list (first wff) ;new call
(first ans-code)))
(actualize (rest wff))))))
(def make-try (trylist) ;gets called with the list of subgoals with
(cond ((null trylist) 'true) ;the "try" stripped off, and generates a
(t ((lambda (call) ;conjunction out of the subgoal calls
(cond ((null (rest trylist))
call)
(t (append call
'(AND)
(make-try (rest trylist))))))
(list (first (first trylist))
(rest (first trylist)))))))
(def stripdeep! (exp)
(cond ((atom exp) ((lambda (namelist)
(cond ((eq (first namelist) '!)
(implode (rest namelist)))
(t exp)))
(explode exp)))
(t (cons (stripdeep! (first exp))
(stripdeep! (rest exp))))))
(def make-body-of (name)
(prog (donelist local-vars pascode)
(setq local-vars '((actuals copyactuals matchlist) () () ()))
(setq donelist (strip! (get name 'params)))
(setq pascode
(append
'(BEGIN /
) pascode
'( if /
)
(list (algol-ize (stripdeep! (get name 'typedprecond))) '/
)
'(then / begin /
)
(build-actuals (strip! (get name 'params)))
(do ((alts (reverse (stripdeep! (rest (get name 'body)))) (rest alts))
(ans () ((lambda (alt)
(setq donelist '(actuals copyactuals matchlist))
(append
'(copyactuals / := / copytermlist (actuals) /; /
new(donetbl)/;/
donetbl↑/.notempty/ :=/ false/;/
standapart (copyactuals/, donetbl)/;/
)
(mk-termlist 'matchlist (match-pt alt))
'(if / unify (copyactuals /, matchlist/, copyactuals/,
matchlist/, failed) /
then / begin /
)
((lambda (sbgls-code)
(append (rest sbgls-code)
(list 'failed '/ ':= '/ 'not '/
(make-try (first sbgls-code)) '/
'end '/
)))
(fix-subgoals (try-pt alt)))
'(else / failed / := / true /; /
)
ans))
(first alts))))
((null alts) ans))
(list 'flag '/ ':= '/ 'not '/ 'failed '/; '/
name '/ ':='/ 'flag'/;'/
'if '/ 'flag '/
'then '/ 'begin '/
)
(mk-assgns (strip! (get name 'params)))
(list 'end '/
'end '/
'else '/ name '/ ':= '/ 'false '/
'end '/;'/
)))
(return
(append
(make-local-decs local-vars)
'(/ donetbl:/ varpairs/;/
/ flag/,/ failed:/ boolean/;/
/
) pascode))))
(def mk-assgns (params)
(cond ((null params) ())
(t (append (list (first params) '/ ':= 'copyactuals↑/.first '/; '/
'copyactuals '/ ':='/ 'copyactuals↑/.rest '/; '/
) (mk-assgns (rest params))))))
;build-actuals generates the pascal code to build a termlist out of the actual
;parameters, the actuals are already of type term, so all it has to do is link
;them together into a termlist called actuals so they will be appropriate input
;to the unifier.
(def build-actuals (params)
(append
(list 'new '(actuals) '/; '/
'actuals↑/.notempty '/ ':= '/ 'false '/; '/
)
(do ((vars params (rest vars))
(ans () ((lambda (temp)
(addlocal-tml temp)
(append
(list 'new '/( temp '/) '/; '/
temp '↑'/.'notempty '/ ':= '/ 'true'/; '/
temp '↑ '/.'first '/ ':= '/ (first vars) '/;'/
temp '↑'/.'rest '/ ':= '/ 'actuals'/; '/
'actuals '/ ':= '/ temp '/; '/
)
ans))
(gensym))))
((null vars) ans))))
(def mk-termlist (name arglist) ;generates the pascal code to make a termlist,
(addlocal-tml name) ;pointed to by name, whose elements are made up
;of terms constructed from the elements of arglist.
;donelist is global (local to make-body) and is
;re-initialized whenever a new alternative is
;being translated. All variables created in this
;process (new'd) must be added to the list local-
;vars so that the appropriate declarations will be
;generated for them.
(append
(list 'new '/( name '/) '/; '/
name '↑ '/. 'notempty '/ ':='/ 'false '/; '/
)
(do ((args (reverse arglist) (rest args))
(ans () ((lambda (temp)
(addlocal-tml temp)
(append
(list 'new '/( temp '/) '/; '/
temp '↑ '/. 'notempty '/ ':='/ 'true '/;'/
)
(cond ((is-var (first args))
(cond ((memq (first args) donelist)
(list temp '↑'/.'first'/ ':='/
(first args)'/;'/
))
(t (mark-done (first args))
(append (mk-term (first args)
(first args))
(list temp '↑'/.'first '/ ':='/
(first args) '/; '/
)))))
(t ((lambda (tmname)
(append (mk-term tmname (first args))
(list temp'↑'/.'first '/ ':='/
tmname '/; '/
)))
(gensym))))
(list temp'↑'/.'rest '/ ':= '/ name '/; '/
name '/ ':='/ temp '/; '/
)
ans))
(gensym))))
((null args) ans))))
(def mk-term (name arg)
(prog (quotflag)
(addlocal-tm name)
(return
(append
(list 'new '/( name '/) '/; '/
)
(cond ((is-var arg)
(list name'↑'/.'ttyp '/ ':= '/ 'variable'/; '/
name '↑'/.'vr '/ ':= '/ 'genvar '/; '/
))
((is-constant arg)
(cond ((is-quoted arg) (setq quotflag t)
(setq arg (second arg))))
(cond ((atom arg)
(append (list name '↑'/.'ttyp '/ ':='/ 'constanttyp'/; '/
) ((lambda (con)
(append
(mk-const con arg)
(list name '↑'/.'cnst '/ ':='/ con'/;'/
)))
(gensym))))
(quotflag
(append (list name'↑'/.'ttyp '/ ':='/ 'funapp'/; '/
) (mk-sym 'cons (explode 'cons))
((lambda (tml)
(append
(mk-termlist tml (rest (cons-out arg)))
(list name'↑'/.'fname'/ ':='/ 'cons '/;'/
name'↑'/.'args '/ ':='/ tml'/; '/
)))
(gensym))))
(t (append
(list name'↑'/.'ttyp '/ ':='/ 'funapp'/; '/
) (mk-sym (first arg) (explode (first arg)))
((lambda (tml)
(mk-termlist tml (rest arg)))
(gensym))
(list name'↑'/.'fname'/ ':='/ (first arg)'/;'/
name'↑'/.'args '/ ':='/ tml'/; '/
)))))
(t (append
(list name'↑'/.'ttyp '/ ':='/ 'funapp'/; '/
) (mk-sym (first arg) (explode (first arg)))
((lambda (tml)
(mk-termlist tml (rest arg)))
(gensym))
(list name'↑'/.'fname'/ ':='/ (first arg)'/;'/
name'↑'/.'args '/ ':='/ tml'/; '/
))))))))
(def cons-out (list)
(cond ((null list) ())
(t (list 'cons (cond ((is-constant (first list)) (first list))
(t (list 'quote (first list))))
(cons-out (rest list))))))
(def mk-const (name atm)
(addlocal-cnst name)
(append (list 'new '/( name '/) '/;'/
)
(cond ((fixp atm) (list name'↑'/.'ctyp '/ ':= '/ 'integertyp'/; '/
name'↑'/.'ival '/ ':= '/ atm '/; '/
))
((floatp atm) (list name'↑'/.'ctyp '/ ':='/ 'real'/; '/
name'↑'/.'rval '/ ':='/ atm '/; '/
))
((eq atm t) (list name'↑'/.'ctyp '/ ':='/ 'boolean'/; '/
name'↑'/.'bval '/ ':= '/ 'true'/; '/
))
((eq atm false) (list name'↑'/.'ctyp '/ ':='/ 'boolean'/; '/
name'↑'/.'bval '/ ':= '/ 'false'/; '/
))
(t (append (list name'↑'/.'ctyp '/ ':='/ 'symbol'/; '/
) (mk-sym arg (explode arg))
(list name'↑'/.'sval '/ ':= '/ arg'/; '/
))))))
(def is-quoted (x) (cond ((atom x) nil)
(t (eq (first x) 'quote))))
(def mk-sym (name charlist)
(cond
((memq name donelist) ())
(t
(addlocal-sym name)
(append (list 'new '/( name '/)'/;'/
name '↑ '/. 'notempty '/ ':='/ 'false'/;'/
)
(do ((chars (reverse charlist) (rest chars))
(ans () ((lambda (temp)
(addlocal-sym temp)
(append
(list 'new '/( temp '/)'/; '/
temp '↑'/.'notempty '/ ':='/ 'true'/;'/
temp '↑'/.'firstch '/ ':='/ (first chars)'/;'/
temp '↑'/.'tail '/ ':='/ name'/; '/
name '/ ':='/ temp '/;'/
)
ans))
(gensym))))
((null chars) ans))))))
(def fix-subgoals (sbglist) ;makes a list of subgoals whose arglists are lists
(cond ;of terms for which the pascal code has been
((null sbglist)'(())) ;generated. its value is the new sbglist cons onto
(t ((lambda (first-ans rest-ans) ;the list of pascal stuff
(cons
(cons (cons (first (first sbglist)) ;i.e., subgoal name
(first first-ans)) ;i.e., new arglist
(first rest-ans)) ;the other subgoals
(append (rest first-ans) ;p-code for this subgoal
(rest rest-ans)))) ;p-code for the rest of the subgoals
(actualize (rest (first sbglist))) ;generates stuff for one arglist
(fix-subgoals (rest sbglist))))))
(def actualize (arglist) ;turns an arglist in intermediate form, into a list
(cond ;of terms- the value is the new arglist cons'd onto
((null arglist)'(())) ;the list of p-code
(t ((lambda (arg-ans rest-ans)
(cons (cons (first arg-ans)
(first rest-ans))
(append (rest arg-ans)
(rest rest-ans))))
(arg-to-term (first arglist))
(actualize (rest arglist))))))
(def arg-to-term (arg)
(cond
((is-var arg)
(cond ((memq arg donelist) (list arg))
(t (cons arg (mk-term arg arg)))))
(t ((lambda (name)
(cons name
(mk-term name arg)))
(gensym)))))
;local-vars and donelist are global to several of the above functions. They are
;the means by which information about which terms have been generated and
;must be declared are transmitted about. Local-vars is a list of 4 lists of
;variables that must be declared as termlists, terms, constants, and symbols,
;respectively. Every time a new variable is created it is added to this list
;in the appropriate type sublist. Whenever a variable (pointer) is created
;that may appear again, it is added to donelist so that multiple versions
;need not be generated.
(def mark-done (name) (setq donelist (cons-if-new name donelist)))
(def addlocal-tml (name)
(setq local-vars (cons (cons-if-new name (first local-vars))
(rest local-vars))))
(def addlocal-tm (name)
(setq local-vars (cons (first local-vars)
(cons (cons-if-new name (second local-vars))
(rest (rest local-vars))))))
(def addlocal-cnst (name)
(setq local-vars (cons (first local-vars)
(cons (second local-vars)
(cons (cons-if-new name (third local-vars))
(rest (rest (rest local-vars))))))))
(def addlocal-sym (name)
(setq local-vars (cons (first local-vars)
(cons (second local-vars)
(cons (third local-vars)
(cons (cons-if-new name (fourth local-vars))
()))))))
.end
.next page
The following programs were written directly in Pascal as part of the implementation
of the "back end" for the language.
.begin nofill;turn off "↑"
(*pascal programs*)
(*$E+*)
program Junk,Unify,Subst,Replace,Copytermlist,Copyterm,Copyconst,Copysym;
(*pascal can't handle things the way it should so we have to invent strange
names that are all referring to the same thing, in particular, the type
of the object at hand. Thus,
alltyps, an indication of the possible atomic types, is actually made
up of convoluted versions of the type names.
this idiocy is carried on throughout, which is why you'll see several
different names that all look similar but had to be different for pascal. *)
TYPE
(* Alltyps are the types of atomic constants *)
Alltyps = (Integertyp, Realtyp, Booleantyp, Chartyp, Symboltyp);
Termtyps = (Variable, Constanttyp, Funapp);
Term = ↑T1;
Termlist = ↑Tl1;
Constant = ↑C1;
Symbol = ↑Sym1;
T1 = record
case Ttyp:Termtyps of
Variable: (Vr: integer);
Constanttyp: (Cnst: Constant);
Funapp: (Fname: Symbol;
Args: Termlist)
end;
Tl1 = record
Notempty: Boolean;
First: Term;
Rest: Termlist
end;
C1 = record
case Ctyp:Alltyps of
Integertyp: (Ival: integer);
Realtyp: (Rval: real);
Booleantyp: (Bval: boolean);
Chartyp: (Cval: char);
Symboltyp: (Sval: Symbol)
end;
Sym1 = record
Notempty: boolean;
Firstch: char;
Tail: Symbol
end;
Varpairs = ↑Vp;
Vp = record
Notempty: boolean;
Old: integer;
New: integer;
Rest: Varpairs
end;
function Genvar:integer;
begin
Genvar:= realtime
end;(*genvar*)
function Occur(X,Y:Term):boolean;
var Ptr: Termlist;
Flag: boolean;
begin
if Y↑.Ttyp = Variable
then begin
if Y↑.Vr = X↑.Vr
then Occur := true
else Occur := false
end
else if Y↑.Ttyp = Constanttyp
then Occur := false
else begin
Ptr := Y↑.Args;
Flag := false;
while Ptr↑.Notempty and (Flag = false)
do begin
Flag := Occur(X, Ptr↑.First);
Ptr := Ptr↑.Rest
end;
Occur := Flag
end
end;(*Occur*)
procedure Replace(X, T: Term; var Tml: Termlist);
var Tl1:Termlist;
T1:Term;
begin
Tl1:= Tml;
while Tl1↑.Notempty do
begin
T1 := Tl1↑.First;
if not(T1↑.Ttyp = Constanttyp)
then begin
if T1↑.Ttyp = Variable
then begin
if X↑.Vr = T1↑.Vr
then
Tl1↑.First := T (*need to mung record, not just ptr t1*)
(*else, no change needed*)
end
else (*it's a funapp*)
Replace(X, T, Tl1↑.First↑.Args)
end;
(*if its a constant no changes need be made*)
Tl1 := Tml↑.Rest
end (*of while*)
end; (*Replace*)
procedure Subst(X, T:Term; var T1, T2:Termlist);
begin
Replace(X, T, T1);
Replace(X, T, T2)
end;
function Eqsym(X,Y:Symbol):boolean;
begin
while X↑.Notempty and Y↑.Notempty and (X↑.Firstch = Y↑.Firstch) do
begin
X:=X↑.Tail;
Y:=Y↑.Tail
end;
if X↑.Notempty or Y↑.Notempty
then Eqsym:= false
else Eqsym:= true
end;
function Eqconst(X,Y:Constant):boolean;
begin
if X↑.Ctyp = Y↑.Ctyp
then case X↑.Ctyp of
Integertyp: Eqconst:= X↑.Ival = Y↑.Ival;
Realtyp: Eqconst:= X↑.Rval = Y↑.Rval;
Booleantyp: Eqconst:= X↑.Bval = Y↑.Bval;
Chartyp: Eqconst:= X↑.Cval = Y↑.Cval;
Symboltyp: Eqconst:= Eqsym(X↑.Sval, Y↑.Sval)
end
else Eqconst:= false
end;
function Copysym(Oldsym:Symbol):Symbol;
var Newsym, Lastnode, Newnode:Symbol;
begin
new(Newsym);
Lastnode := Newsym;
while Oldsym↑.Notempty do
begin
Lastnode↑.Notempty := true;
Lastnode↑.Firstch := Oldsym↑.Firstch;
new(Newnode);
Lastnode↑.Tail := Newnode;
Lastnode := Newnode;
Oldsym := Oldsym↑.Tail
end;
Lastnode↑.Notempty := false;
Copysym := Newsym
end; (*Copysym*)
function Copyterm(Oldtm:Term):Term;
forward;
function Copytermlist(Tml:Termlist):Termlist;
var Newnode, Lastnode, Tmlnew:Termlist;
begin
new(Tmlnew);
Lastnode := Tmlnew;
while Tml↑.Notempty do
begin
Lastnode↑.Notempty := true;
Lastnode↑.First := Copyterm(Tml↑.First);
new(Newnode);
Lastnode↑.Rest := Newnode;
Lastnode := Newnode;
Tml := Tml↑.Rest;
end;
Lastnode↑.Notempty := false;
Copytermlist := Tmlnew
end; (*Copytermlist*)
function Copyconst(Oldconst:Constant):Constant;
var Newconst:Constant;
begin
new(Newconst);
Newconst↑.Ctyp := Oldconst↑.Ctyp;
case Newconst↑.Ctyp of
Integertyp: Newconst↑.Ival := Oldconst↑.Ival;
Realtyp: Newconst↑.Rval := Oldconst↑.Rval;
Booleantyp: Newconst↑.Bval := Oldconst↑.Bval;
Chartyp: Newconst↑.Cval := Oldconst↑.Cval;
Symboltyp: Newconst↑.Sval := Copysym(Oldconst↑.Sval)
end; (*of case stmt*)
Copyconst := Newconst
end; (*Copyconst*)
function Copyterm;
var Newtm:Term;
begin
new(Newtm);
Newtm↑.Ttyp := Oldtm↑.Ttyp;
case Newtm↑.Ttyp of
Variable: Newtm↑.Vr := Oldtm↑.Vr; (*it's just an integer*)
Constanttyp: Newtm↑.Cnst := Copyconst(Oldtm↑.Cnst);
Funapp: begin
Newtm↑.Fname := Copysym(Oldtm↑.Fname);
Newtm↑.Args := Copytermlist(Oldtm↑.Args)
end
end; (*of case stmt*)
Copyterm := Newtm
end; (*Copyterm*)
(*the first call on unify will repeat the arglists being unified- dumb, but it
makes it possible to accomplish the substitutions by replacement as we go instead
of building a substitution and making new copies of everything every time we do
a substitution. the allx and ally args are necessary to ensure that any replacements
resulting from recursive calls get made throughout the entire termlists you started
with*)
function Unify(var X, Y, Allx, Ally: Termlist; Failed:boolean): boolean;
var X1, Y1: Termlist;
X2, Y2: Term;
Dummy, Subfailed: boolean;
begin
(*initialize*)
Failed := False;
X1 := X;
Y1 := Y;
while X1↑.Notempty and Y1↑.Notempty and not(Failed) do
begin
X2 := X1↑.First;
Y2 := Y1↑.First;
if X2↑.Ttyp = Variable
then begin
if Y2↑.Ttyp = Variable
then X2↑.Vr := Y2↑.Vr
(* if they're already the same, the assignment is unnecessary
but cheaper than testing the equality and won't hurt anything*)
else if Occur(X2, Y2)
then Failed := true
else Subst(X2, Y2, X, Y)
end
else if Y2↑.Ttyp = Variable
then begin
if Occur(Y2, X2)
then Failed := true
else Subst(Y2, X2, X, Y)
end
else if X2↑.Ttyp = Constanttyp
then begin
if Y2↑.Ttyp = Constanttyp
then begin
if not( Eqconst(X2↑.Cnst, Y2↑.Cnst) )
then Failed := true;
(*if they are = nothing need be done*)
end
else Failed := true
end
else (*X2 is a funapp and Y2 is not a variable*)
if Y2↑.Ttyp = Constanttyp
then Failed := true
else (*X2 and Y2 are both funapp terms*)
if Eqsym(X2↑.Fname, Y2↑.Fname)
then begin
Dummy :=
Unify(X2↑.Args, Y2↑.Args,
Allx, Ally, Subfailed);
if Subfailed
then Failed := true
end
else Failed :=true;
X1 := X1↑.Rest;
Y1 := Y1↑.Rest
end; (*of while*)
if X1↑.Notempty or Y1↑.Notempty then Failed := true;
Unify := not Failed
end; (*Unify*)
function Lessthan(X, Y:Term; var Z:Term):boolean;
var Con: Constant;
begin
Z↑.Ttyp := Constanttyp;
new(Con);
Z↑.Cnst := Con;
Con↑.Ctyp := Booleantyp;
if X↑.Cnst↑.Ival < Y↑.Cnst↑.Ival
then Z↑.Cnst↑.Bval := true
else Z↑.Cnst↑.Bval := false;
Lessthan := true
end;
function Greaterequal(X, Y:Term; var Z: Term): boolean;
var Con: Constant;
begin
Z↑.Ttyp := Constanttyp;
new(Con);
Con↑.Ctyp := Booleantyp;
Z↑.Cnst := Con;
if X↑.Cnst↑.Ival >= Y↑.Cnst↑.Ival
then Z↑.Cnst↑.Bval := true
else Z↑.Cnst↑.Bval := false;
Greaterequal := true
end;
function Times(X, Y:Term; var Z:Term): boolean;
var Con:Constant;
begin
Z↑.Ttyp := Constanttyp;
new(Con);
Con↑.Ctyp := Integertyp;
Z↑.Cnst := Con;
Con↑.Ival := X↑.Cnst↑.Ival * Y↑.Cnst↑.Ival;
Times := true
end;
function Sub1(X: Term; var Y:Term):boolean;
var Con:Constant;
begin
Y↑.Ttyp := Constanttyp;
new(Con);
Con↑.Ctyp := Integertyp;
Y↑.Cnst := Con;
Con↑.Ival := X↑.Cnst↑.Ival - 1;
Sub1 := true
end;
procedure Lookup(Tm:Term; Tbl: Varpairs; Found: boolean);
var Ptr: Varpairs;
begin
Found := false;
Ptr := Tbl;
while Ptr↑.Notempty and not Found
do begin
if Ptr↑.Old = Tm↑.Vr
then begin
Tm↑.Vr := Ptr↑.New;
Found := true
end;
Ptr := Ptr↑.Rest
end
end; (*Lookup*)
procedure Standapart(Tml: Termlist; var Donetbl: Varpairs);
var Ptr: Termlist;
Done: Varpairs;
Found: boolean;
begin
Ptr:= Tml;
while Ptr↑.Notempty
do begin
if Ptr↑.First↑.Ttyp = Variable
then begin
Lookup(Ptr↑.First, Donetbl, Found);
if not Found
then begin
new(Done);
Done↑.Notempty := true;
Done↑.Old := Ptr↑.First↑.Vr;
Done↑.New := Genvar;
Ptr↑.First↑.Vr := Done↑.New;
Done↑.Rest := Donetbl;
Donetbl := Done
end
end
else if Ptr↑.First↑.Ttyp = Funapp
then Standapart(Ptr↑.First↑.Args, Donetbl);
Ptr := Ptr↑.Rest
end
end; (*Standapart*)
begin (*Junk, ie, main program*)
end.
.end